Commit 2023-02-07 08:39 12ec4c91

View on Github →

feat: port Topology.Sober (#2134)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

added theorem closure_image_closure

Created Mathlib/Topology/Sober.lean

added theorem ClosedEmbedding.quasiSober

added theorem IsGenericPoint.def

added theorem IsGenericPoint.disjoint_iff

added theorem IsGenericPoint.mem_closed_set_iff

added theorem IsGenericPoint.mem_open_set_iff

added theorem IsGenericPoint.specializes_iff_mem

added def IsGenericPoint

added theorem IsIrreducible.genericPoint_closure_eq

added theorem IsIrreducible.genericPoint_spec

added theorem OpenEmbedding.quasiSober

added theorem genericPoint_closure

added theorem genericPoint_spec

added theorem genericPoint_specializes

added theorem isGenericPoint_closure

added theorem isGenericPoint_def

added theorem isGenericPoint_iff_forall_closed

added theorem isGenericPoint_iff_specializes

added theorem quasiSober_of_open_cover

Modified Mathlib/Topology/SubsetProperties.lean