disjoint_ofDual_iff — Mathlib

English

If a' and b' are dual elements, then Codisjoint (ofDual a') (ofDual b') corresponds to Disjoint a' b' in the original lattice.

Русский

Если a' и b' — двойственные элементы, то Codisjoint (ofDual a') (ofDual b') соответствует Disjoint a' b' в исходной решётке.

LaTeX

$$$\text{Codisjoint}({a^*}, {b^*)} \iff \text{Disjoint}(a,b)$$$

Lean4

@[simp]
theorem disjoint_ofDual_iff [PartialOrder α] [OrderBot α] {a b : αᵒᵈ} :
    Disjoint (ofDual a) (ofDual b) ↔ Codisjoint a b :=
  Iff.rfl

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