Commit 2023-03-11 14:46 f6189baf

View on Github →

feat: port CategoryTheory.Limits.Lattice (#2787)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Lattice.lean

added def CategoryTheory.Limits.CompleteLattice.colimitCocone

added theorem CategoryTheory.Limits.CompleteLattice.colimit_eq_supᵢ

added theorem CategoryTheory.Limits.CompleteLattice.coprod_eq_sup

added def CategoryTheory.Limits.CompleteLattice.finiteColimitCocone

added def CategoryTheory.Limits.CompleteLattice.finiteLimitCone

added theorem CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup

added theorem CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup

added theorem CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf

added theorem CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf

added def CategoryTheory.Limits.CompleteLattice.limitCone

added theorem CategoryTheory.Limits.CompleteLattice.limit_eq_infᵢ

added theorem CategoryTheory.Limits.CompleteLattice.prod_eq_inf

added theorem CategoryTheory.Limits.CompleteLattice.pullback_eq_inf

added theorem CategoryTheory.Limits.CompleteLattice.pushout_eq_sup