isCompl_iff — Mathlib

English

IsCompl x y in Ici a iff Disjoint x.val y.val and x.val ⊔ y.val = a.

Русский

IsCompl x y в Ici a эквивалентно Disjoint x.val y.val и x.val ⊔ y.val = a.

LaTeX

$$$$IsCompl x y \\iff (Disjoint x^{\\uparrow} y^{\\uparrow}) \\land (x^{\\uparrow} \\vee y^{\\uparrow}) = a.$$$$

Lean4

protected theorem isCompl_iff [Lattice α] [OrderTop α] {a : α} {x y : Ici a} :
    IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint (x : α) (y : α) := by
  rw [_root_.isCompl_iff, Ici.disjoint_iff, Ici.codisjoint_iff]

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