Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-20 13:27 e473898e

View on Github →

feat(category_theory/glue_data): Some more API for glue_data (#10881)

Estimated changes

Modified src/category_theory/glue_data.lean

added def category_theory.glue_data.V_pullback_cone

added def category_theory.glue_data.V_pullback_cone_is_limit_of_map

added def category_theory.glue_data.glued_iso

added theorem category_theory.glue_data.has_colimit_map_glue_data_diagram

added theorem category_theory.glue_data.has_colimit_multispan_comp

added theorem category_theory.glue_data.types_ι_jointly_surjective

added theorem category_theory.glue_data.types_π_surjective

added theorem category_theory.glue_data.ι_glued_iso_hom

added theorem category_theory.glue_data.ι_glued_iso_inv

added theorem category_theory.glue_data.ι_jointly_surjective