Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-07 14:24 3b7a783f

View on Github →

feat(topology/*): Gluing topological spaces (#9864)

Estimated changes

Modified src/algebraic_geometry/properties.lean

Created src/category_theory/concrete_category/elementwise.lean

Modified src/category_theory/limits/concrete_category.lean

Modified src/category_theory/limits/shapes/concrete_category.lean

Modified src/logic/function/basic.lean

added theorem inv_image.equivalence

Created src/topology/gluing.lean

added theorem Top.glue_data.eqv_gen_of_π_eq

added def Top.glue_data.from_open_subsets_glue

added theorem Top.glue_data.from_open_subsets_glue_injective

added theorem Top.glue_data.from_open_subsets_glue_is_open_map

added theorem Top.glue_data.from_open_subsets_glue_open_embedding

added theorem Top.glue_data.image_inter

added theorem Top.glue_data.is_open_iff

added def Top.glue_data.mk'

added def Top.glue_data.mk_core.t'

added theorem Top.glue_data.mk_core.t_inv

added structure Top.glue_data.mk_core

added def Top.glue_data.of_open_subsets

added def Top.glue_data.open_cover_glue_homeo

added theorem Top.glue_data.open_image_open

added theorem Top.glue_data.preimage_image_eq_image'

added theorem Top.glue_data.preimage_image_eq_image

added theorem Top.glue_data.preimage_range

added theorem Top.glue_data.range_from_open_subsets_glue

added def Top.glue_data.rel

added theorem Top.glue_data.rel_equiv

added theorem Top.glue_data.ι_eq_iff_rel

added theorem Top.glue_data.ι_from_open_subsets_glue

added theorem Top.glue_data.ι_injective

added theorem Top.glue_data.ι_jointly_surjective

added theorem Top.glue_data.ι_open_embedding

added theorem Top.glue_data.π_surjective

added structure Top.glue_data