Theorem Topology.IsOpenEmbedding.uliftMap

Modification history

2026-02-09 14:35
Mathlib/Topology/Homeomorph/Lemmas.lean
feat(Topology/Category): the standard Grothendieck topology on `TopCat` (#34979) …
Added Topology.IsOpenEmbedding.uliftMapView on Github →