Commit 2023-05-21 15:37 a4c11e86

View on Github →

feat: port Topology.Algebra.Module.LocallyConvex (#3637)

Estimated changes

Modified Mathlib.lean

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

added theorem Disjoint.exists_open_convexes

added theorem LocallyConvexSpace.convex_basis_zero

added theorem LocallyConvexSpace.convex_open_basis_zero

added theorem LocallyConvexSpace.ofBases

added theorem LocallyConvexSpace.ofBasisZero

added theorem locallyConvexSpace_iInf

added theorem locallyConvexSpace_iff

added theorem locallyConvexSpace_iff_exists_convex_subset

added theorem locallyConvexSpace_iff_exists_convex_subset_zero

added theorem locallyConvexSpace_iff_zero

added theorem locallyConvexSpace_induced

added theorem locallyConvexSpace_inf

added theorem locallyConvexSpace_sInf