Theorems · Inductive type · order theory

CompleteLattice.MulticoequalizerDiagram

{T : Type u} → [CompleteLattice T] → {ι : Type u_1} → T → (ι → T) → (ι → ι → T) → Prop

A multicoequalizer diagram in a complete lattice T consists of families of elements u : ι → T, v : ι → ι → T, and an element x : T such that x is the supremum of u, and for any i and j, v i j is the minimum of u i and u j.

Defined in

Mathlib.Order.CompleteLattice.MulticoequalizerDiagram

Cited by

9 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CompleteLattice