Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-20 13:27 ab654e5c

View on Github →

feat(topology/sober): Specialization & generic points & sober spaces (#10914)

Estimated changes

Modified src/topology/basic.lean

added theorem is_closed.mem_iff_closure_subset

Modified src/topology/maps.lean

added theorem closed_embedding.closure_image_eq

Modified src/topology/separation.lean

added theorem indistinguishable.eq

added theorem is_irreducible_iff_singleton

added theorem is_preirreducible_iff_subsingleton

Created src/topology/sober.lean

added theorem closed_embedding.sober

added theorem continuous_map.map_specialization

added def generic_point

added theorem generic_point_closure

added theorem generic_point_spec

added theorem generic_point_specializes

added theorem indistinguishable_iff_specializes_and

added def irreducible_set_equiv_points

added theorem is_generic_point.def

added theorem is_generic_point.disjoint_iff

added theorem is_generic_point.eq

added theorem is_generic_point.image

added theorem is_generic_point.is_closed

added theorem is_generic_point.is_irreducible

added theorem is_generic_point.mem

added theorem is_generic_point.mem_closed_set_iff

added theorem is_generic_point.mem_open_set_iff

added theorem is_generic_point.specializes

added def is_generic_point

added theorem is_generic_point_closure

added theorem is_generic_point_def

added def is_irreducible.generic_point

added theorem is_irreducible.generic_point_closure_eq

added theorem is_irreducible.generic_point_spec

added theorem open_embedding.sober

added theorem sober_of_open_cover

added theorem specialization_order.monotone_of_continuous

added def specialization_order

added def specialization_preorder

added theorem specializes.eq

added theorem specializes.map

added theorem specializes.trans

added def specializes

added theorem specializes_antisymm

added theorem specializes_def

added theorem specializes_iff_closure_subset

added theorem specializes_iff_eq

added theorem specializes_iff_forall_closed

added theorem specializes_iff_forall_open

added theorem specializes_refl

added theorem specializes_rfl

Modified src/topology/subset_properties.lean

added theorem irreducible_space.is_irreducible_univ

added theorem is_preirreducible.interior

added theorem is_preirreducible.open_subset

added theorem is_preirreducible.preimage

added theorem is_preirreducible.subset_irreducible

added theorem is_preirreducible_of_subsingleton

added theorem subset_closure_inter_of_is_preirreducible_of_is_open