Theorem OpenEmbedding.quasiSober

Modification history

2024-10-18 21:29

Mathlib/Topology/Sober.lean

chore: Rename `OpenEmbedding` to `IsOpenEmbedding` (#17898) …

Deleted OpenEmbedding.quasiSober View on Github →

2023-02-07 08:39

Mathlib/Topology/Sober.lean

feat: port Topology.Sober (#2134)

Added OpenEmbedding.quasiSober View on Github →