Commit 2025-09-21 19:07 c822477a

View on Github →

feat(Topology/Maps): IsOpenMap and ClusterPt (#23240)

Estimated changes

Modified Mathlib/Topology/ClusterPt.lean

added theorem mem_interior_iff_not_clusterPt_compl

Modified Mathlib/Topology/Maps/Basic.lean

added theorem Topology.IsInducing.IsOpenMap.clusterPt_comap

added theorem Topology.IsInducing.isOpenMap_iff_clusterPt_comap