Mathlib Map

Theorems · Definition · order theory

CompleteLattice.MulticoequalizerDiagram.multispanIndex

{T : Type u} →
  [inst : CompleteLattice T] →
    {ι : Type u_1} →
      {x : T} →
        {u : ι → T} →
          {v : ι → ι → T} →
            CompleteLattice.MulticoequalizerDiagram x u v →
              CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) T

The multispan index in the category associated to the complete lattice T given by the objects u i and the minima v i j = u i ⊓ u j, when d : MulticoequalizerDiagram x u v.

Defined in
Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Cited by
20 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CompleteLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.horn₃₁.desc.multicofork · cited by 10desc.multicoforkSSet.horn₃₂.desc.multicofork · cited by 10desc.multicoforkSSet.horn.isColimit · cited by 8horn.isColimitCompleteLattice.MulticoequalizerDiagram.multicofork · cited by 4MulticoequalizerDiagram.m…SSet.horn₃₁.desc.multicofork_π_three · cited by 1desc.multicofork_π_threeSSet.horn₃₁.desc.multicofork_π_two · cited by 1desc.multicofork_π_twoSSet.horn₃₁.desc.multicofork_π_zero · cited by 1desc.multicofork_π_zeroCategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram' · cited by 1Types.isColimitOfMulticoe…SSet.horn₃₂.desc.multicofork_π_one · cited by 1desc.multicofork_π_oneSSet.horn₃₂.desc.multicofork_π_three · cited by 1desc.multicofork_π_threeSSet.horn₃₂.desc.multicofork_π_zero · cited by 1desc.multicofork_π_zeroSSet.horn₃₁.desc.multicofork_pt · cited by 0desc.multicofork_ptSSet.horn₃₁.desc.multicofork_π_three_assoc · cited by 0desc.multicofork_π_three_…SSet.horn₃₁.desc.multicofork_π_two_assoc · cited by 0desc.multicofork_π_two_as…CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram · cited by 0Types.isColimitOfMulticoe…CompleteLattice · cited by 1048CompleteLatticeCategoryTheory.homOfLE · cited by 554CategoryTheory.homOfLECategoryTheory.Limits.MultispanShape.L · cited by 129MultispanShape.LCategoryTheory.Limits.MultispanIndex · cited by 102Limits.MultispanIndexCategoryTheory.Limits.MultispanShape.prod · cited by 93MultispanShape.prodCompleteLattice.MulticoequalizerDiagram · cited by 9CompleteLattice.Multicoeq…MulticoequalizerDiagram.multi…CITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by28

Results whose statement or proof uses this declaration.