Commit 2024-01-14 01:19 b12f3dad

View on Github →

chore(LocallyConvex/Bounded): rename a lemma (#9712) Rename Filter.HasBasis.isVonNBounded_basis_iff to Filter.HasBasis.isVonNBounded_iff. It already has basis in the namespace.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

deleted theorem Filter.HasBasis.isVonNBounded_basis_iff

added theorem Filter.HasBasis.isVonNBounded_iff

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean