isCompl_iff — Mathlib

English

Within a lattice α, and a ≤ b, two elements x,y in Icc(a,b) are complementary iff their images satisfy the standard complement equations: x ⊓ y = a and x ⊔ y = b.

Русский

Для элементов x,y внутри Icc(a,b) комплементарность эквивалентна выполнению обычных уравнений: x ⊓ y = a и x ⊔ y = b.

LaTeX

$$$\text{IsCompl}(x,y) \iff x^{\uparrow} \! \inf y^{\uparrow} = a \ \\ \text{ and } \ x^{\uparrow} \! \sup y^{\uparrow} = b$$$

Lean4

protected theorem isCompl_iff [Lattice α] [Fact (a ≤ b)] {x y : Icc a b} : IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b := by
  rw [_root_.isCompl_iff, Icc.disjoint_iff, Icc.codisjoint_iff]

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