disjoint_iff — Mathlib

English

For x,y ∈ Icc(a,b) with SemilatticeInf on α and a ≤ b, Disjoint(x,y) holds iff the infimum of their α-values equals a, i.e., x.1 ⊓ y.1 = a.

Русский

Для x,y ∈ Icc(a,b) при наличии SemilatticeInf на α, выполняется Disjoint(x,y) тогда и только тогда, когда их значения в α имеютInf равный a: x.1 ⊓ y.1 = a.

LaTeX

$$$\text{Disjoint}(x,y) \quad\iff\quad x^{\uparrow} \! \inf y^{\uparrow} = a \,$$$

Lean4

protected theorem disjoint_iff [SemilatticeInf α] [Fact (a ≤ b)] {x y : Icc a b} : Disjoint x y ↔ ↑x ⊓ ↑y = a := by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

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