Commit 2023-06-20 01:57 ab415df4

View on Github →

feat: interaction between StarSubalgebra.map and topologicalClosure (#5166)

Estimated changes

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

added theorem StarSubalgebra.map_topologicalClosure_le

added theorem StarSubalgebra.topologicalClosure_map

added theorem StarSubalgebra.topologicalClosure_map_le