Theorems · Theorem · order theory

CompleteLattice.MulticoequalizerDiagram.multispanIndex_left

∀ {T : Type u} [inst : CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T}
  (d : CompleteLattice.MulticoequalizerDiagram x u v) (x_1 : (CategoryTheory.Limits.MultispanShape.prod ι).L),
  d.multispanIndex.left x_1 =
    match x_1 with
    | (i, j) => v i j

Defined in

Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice