Theorem Topology.IsInducing.IsOpenMap.clusterPt_comap

Modification history

2025-09-21 19:07
Mathlib/Topology/Maps/Basic.lean
feat(Topology/Maps): `IsOpenMap` and `ClusterPt` (#23240)
Added Topology.IsInducing.IsOpenMap.clusterPt_comapView on Github →