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.
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.