English
There is a construction, mk', producing a lattice congruence on α from a relation r on α that is reflexive and satisfies compatibility with the lattice operations and transitivity stipulated by the axioms; this yields a legitimate LatticeCon α.
Русский
Существует конструкция mk', задающая конгруэнцию решётки на α из отношения r на α, если r рефлексивно, совместимо с операциями ∧ и ∨ и удовлетворяет требуемой транзитивности; получается корректная LatticeCon α.
LaTeX
$$$\\text{There exists a } LatticeCon(\\alpha) \\text{ with } r, \\text{ refl, and compatibility conditions as specified.}$$$
Lean4
/-- Alternative conditions for a lattice congruence. -/
def mk' [Lattice α] (r : α → α → Prop) [h₁ : IsRefl α r] (h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y))
(h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z)
(h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)) : LatticeCon α
where
r := r
iseqv.refl := h₁.refl
iseqv.symm h := by simpa [h₂, inf_comm, sup_comm, ← h₂] using h
iseqv.trans hxy hxz := transitive h₂ h₃ h₄ hxy hxz
inf := by
intro w _ _ _ h1 h2
have compatible_left_inf {x y t : α} (hh : r x y) : r (x ⊓ t) (y ⊓ t) :=
closed_interval h₂ h₄ ((x ⊓ y) ⊓ t) _ _ ((x ⊔ y) ⊓ t) (inf_le_inf_right _ inf_le_left)
(inf_le_inf_right _ le_sup_left) (inf_le_inf_right _ inf_le_right) (inf_le_inf_right _ le_sup_right)
(h₄ inf_le_sup (h₂.mp hh)).1
exact transitive h₂ h₃ h₄ (by simpa [inf_comm w] using compatible_left_inf h2) (compatible_left_inf h1)
sup := by
intro w _ _ _ h1 h2
have compatible_left_sup {x y t : α} (hh : r x y) : r (x ⊔ t) (y ⊔ t) :=
closed_interval h₂ h₄ ((x ⊓ y) ⊔ t) _ _ ((x ⊔ y) ⊔ t) (sup_le_sup_right inf_le_left _)
(sup_le_sup_right le_sup_left _) (sup_le_sup_right inf_le_right _) (sup_le_sup_right le_sup_right _)
(h₄ inf_le_sup (h₂.mp hh)).2
exact transitive h₂ h₃ h₄ (by simpa [sup_comm w] using compatible_left_sup h2) (compatible_left_sup h1)
