Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-21 13:06 4a8c38e4

View on Github →

chore(category_theory/limits/lattice): cleanup (#4191)

Estimated changes

Modified src/category_theory/limits/lattice.lean

added def category_theory.limits.complete_lattice.colimit_cocone

added def category_theory.limits.complete_lattice.colimit_iso_supr

added theorem category_theory.limits.complete_lattice.colimit_iso_supr_hom

added theorem category_theory.limits.complete_lattice.colimit_iso_supr_inv

added def category_theory.limits.complete_lattice.limit_cone

added def category_theory.limits.complete_lattice.limit_iso_infi

added theorem category_theory.limits.complete_lattice.limit_iso_infi_hom

added theorem category_theory.limits.complete_lattice.limit_iso_infi_inv