Commit 2025-05-07 13:08 68b54a49

View on Github →

chore(Filter/Bases,LocallyConvex): use new-style dot notation (#24604)

Estimated changes

Modified Mathlib/Order/Filter/Bases/Finite.lean

deleted theorem Filter.hasBasis_iInf'

deleted theorem Filter.hasBasis_iInf

Modified Mathlib/Order/Filter/CountablyGenerated.lean

Modified Mathlib/Order/Filter/Pi.lean

Modified Mathlib/Topology/Algebra/Module/LocallyConvex.lean

deleted theorem locallyConvexSpace_iInf

deleted theorem locallyConvexSpace_induced

deleted theorem locallyConvexSpace_inf

deleted theorem locallyConvexSpace_sInf

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Separation/Regular.lean

Modified Mathlib/Topology/UniformSpace/Ultra/Constructions.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean