English
The multicofork associated to a complete lattice multicoequalizer diagram is defined by apex x and legs given by homOfLE along left/right components, forming a cone with specified maps.
Русский
Кофорка множества, связанная с многообразной диаграммой в CompleteLattice, задаётся вершиной x и рёбрами, заданными через homOfLE по левым/правым компонентам, образуя конус с соответствующими отображениями.
LaTeX
$$$\\text{multicofork}(d) = \\mathrm{Multicofork.of\\pi}\\;\\_\\; x\\; (i \\mapsto \\mathrm{homOfLE}(\\text{by grind}))\\;(\\_; \\mapsto \\mathrm{rfl})$$$
Lean4
theorem multicoequalizerDiagram {T : Type u} [CompleteLattice T] {x₁ x₂ x₃ x₄} (sq : BicartSq x₁ x₂ x₃ x₄) :
CompleteLattice.MulticoequalizerDiagram (T := T) x₄ (fun i ↦ bif i then x₃ else x₂)
(fun i j ↦ bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂)
where
iSup_eq := by rw [← sq.max_eq, sup_comm, sup_eq_iSup]
min_eq i j := by grind [inf_idem, inf_comm]
