Def TopCat.isOpenEmbedding

Modification history

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