isCompl_iff — Mathlib

English

IsCompl x y in Iic(a) iff Disjoint x.val y.val and x.val ⊔ y.val = a.

Русский

IsCompl x y в Iic(a) эквивалентно тому, что x.val и y.val частично несовместны и их сумма равна a.

LaTeX

$$$$IsCompl(x,y) \\iff \\bigl(Disjoint(x^{\\uparrow}, y^{\\uparrow}) \\wedge (x^{\\uparrow} \\vee y^{\\uparrow}) = a\\bigr).$$$$

Lean4

protected theorem isCompl_iff [Lattice α] [OrderBot α] {x y : Iic a} :
    IsCompl x y ↔ Disjoint (x : α) (y : α) ∧ ↑x ⊔ ↑y = a := by
  rw [_root_.isCompl_iff, Iic.disjoint_iff, Iic.codisjoint_iff]

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