Commit 2024-07-03 09:27 a25f1f97

View on Github →

feat(Topology/Inseparable): Define specializing maps between topological spaces (#14001) A port of https://github.com/leanprover-community/mathlib/pull/17113

Estimated changes

Modified Mathlib/Order/UpperLower/Basic.lean

added theorem Relation.Fibration.isLowerSet_image

added theorem Relation.Fibration.isUpperSet_image

added theorem Relation.fibration_iff_image_Ici

added theorem Relation.fibration_iff_image_Iic

added theorem Relation.fibration_iff_isLowerSet_image

added theorem Relation.fibration_iff_isLowerSet_image_Iic

added theorem Relation.fibration_iff_isUpperSet_image

added theorem Relation.fibration_iff_isUpperSet_image_Ici

added theorem lowerClosure_eq

added theorem upperClosure_eq

Modified Mathlib/Topology/Inseparable.lean

modified theorem Continuous.specialization_monotone

added theorem GeneralizingMap.stableUnderGeneralization_image

added theorem GeneralizingMap.stableUnderGeneralization_range

added def GeneralizingMap

added theorem GeneralizingMap_iff_stableUnderGeneralization_image

added theorem Inducing.generalizingMap

added theorem Inducing.specializingMap

added theorem IsClosed.stableUnderSpecialization

added theorem IsClosedMap.specializingMap

added theorem IsOpen.stableUnderGeneralization

added theorem OpenEmbedding.generalizingMap

added theorem SpecializingMap.stableUnderSpecialization_image

added theorem SpecializingMap.stableUnderSpecialization_range

added def SpecializingMap

added theorem StableUnderGeneralization.preimage

added def StableUnderGeneralization

added theorem StableUnderSpecialization.preimage

added def StableUnderSpecialization

added theorem Union_closure_singleton_eq_iff

added theorem closure_singleton_eq_Iic

added theorem specializingMap_iff_closure_singleton

added theorem specializingMap_iff_closure_singleton_subset

added theorem specializingMap_iff_isClosed_image_closure_singleton

added theorem specializingMap_iff_stableUnderSpecialization_image

added theorem specializingMap_iff_stableUnderSpecialization_image_singleton

added theorem stableUnderGeneralization_compl_iff

added theorem stableUnderGeneralization_empty

added theorem stableUnderGeneralization_iInter

added theorem stableUnderGeneralization_iUnion

added theorem stableUnderGeneralization_iff_exists_sInter_eq

added theorem stableUnderGeneralization_sInter

added theorem stableUnderGeneralization_sUnion

added theorem stableUnderGeneralization_univ

added theorem stableUnderSpecialization_compl_iff

added theorem stableUnderSpecialization_empty

added theorem stableUnderSpecialization_iInter

added theorem stableUnderSpecialization_iUnion

added theorem stableUnderSpecialization_iff_Union_eq

added theorem stableUnderSpecialization_iff_exists_sUnion_eq

added theorem stableUnderSpecialization_sInter

added theorem stableUnderSpecialization_sUnion

added theorem stableUnderSpecialization_univ