Commit 2021-04-07 15:23 893173d6

View on Github →

feat(category/subobject): complete_lattice instance (#6809)

Estimated changes

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

added def category_theory.limits.wide_pullback_shape.mk_cone

added def category_theory.limits.wide_pushout_shape.mk_cocone

Modified src/category_theory/subobject/basic.lean

added theorem category_theory.subobject.arrow_congr

Modified src/category_theory/subobject/lattice.lean

added def category_theory.subobject.Inf

added theorem category_theory.subobject.Inf_le

added def category_theory.subobject.Sup

added theorem category_theory.subobject.Sup_le

added theorem category_theory.subobject.le_Inf

added def category_theory.subobject.le_Inf_cone

added theorem category_theory.subobject.le_Inf_cone_π_app_none

added theorem category_theory.subobject.le_Sup

added def category_theory.subobject.small_coproduct_desc

added theorem category_theory.subobject.symm_apply_mem_iff_mem_image

added def category_theory.subobject.wide_cospan

added theorem category_theory.subobject.wide_cospan_map_term

added def category_theory.subobject.wide_pullback

added def category_theory.subobject.wide_pullback_ι

Modified src/category_theory/subobject/mono_over.lean

modified def category_theory.mono_over.arrow

added theorem category_theory.mono_over.mk'_coe'

Modified src/measure_theory/measure_space.lean