Commit 2023-06-14 11:40 78426b9c

View on Github →

feat: port Topology.Gluing (#3987)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

Created Mathlib/Topology/Gluing.lean

added def TopCat.GlueData.MkCore.t'

added theorem TopCat.GlueData.MkCore.t_inv

added structure TopCat.GlueData.MkCore

added def TopCat.GlueData.Rel

added theorem TopCat.GlueData.eqvGen_of_π_eq

added def TopCat.GlueData.fromOpenSubsetsGlue

added theorem TopCat.GlueData.fromOpenSubsetsGlue_injective

added theorem TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap

added theorem TopCat.GlueData.fromOpenSubsetsGlue_openEmbedding

added theorem TopCat.GlueData.image_inter

added theorem TopCat.GlueData.isOpen_iff

added def TopCat.GlueData.mk'

added def TopCat.GlueData.ofOpenSubsets

added def TopCat.GlueData.openCoverGlueHomeo

added theorem TopCat.GlueData.open_image_open

added theorem TopCat.GlueData.preimage_image_eq_image'

added theorem TopCat.GlueData.preimage_image_eq_image

added theorem TopCat.GlueData.preimage_range

added theorem TopCat.GlueData.range_fromOpenSubsetsGlue

added theorem TopCat.GlueData.rel_equiv

added theorem TopCat.GlueData.ι_eq_iff_rel

added theorem TopCat.GlueData.ι_fromOpenSubsetsGlue

added theorem TopCat.GlueData.ι_injective

added theorem TopCat.GlueData.ι_jointly_surjective

added theorem TopCat.GlueData.ι_openEmbedding

added theorem TopCat.GlueData.π_surjective

added structure TopCat.GlueData