r_inf_sup_iff — Mathlib

English

In any lattice, for a lattice congruence c, the relation of x and y is determined by the relation of x ∧ y and x ∨ y: c(x ∧ y, x ∨ y) iff c(x, y).

Русский

В любой решётке для конгруэнции c выполнение отношения между x и y эквивалентно выполнению отношения между x ∧ y и x ∨ y: c(x ∧ y, x ∨ y) ⇔ c(x, y).

LaTeX

$$$c.r\\,(x \\wedge y)\\,(x \\vee y) \\,\\Leftrightarrow \\, c.r\\,x\\,y$$$

Lean4

@[simp]
theorem r_inf_sup_iff (c : LatticeCon α) {x y : α} : c.r (x ⊓ y) (x ⊔ y) ↔ c.r x y
    where
  mp h := c.trans (by simpa using c.inf (c.refl x) (c.symm h)) (by simpa using c.inf h (c.refl y))
  mpr h := c.trans (by simpa using c.inf h (c.refl y)) (by simpa using c.sup (c.symm h) (c.refl y))

Похожие утверждения