disjoint_toDual_iff — Mathlib

English

In a lattice with duality, disjointness corresponds to codisjointness when passing to the dual lattice.

Русский

В решётке с двойственным порядком диссообщение соответствует кодиссоединению при переходе к двойственной решётке.

LaTeX

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

Lean4

@[simp]
theorem disjoint_toDual_iff [PartialOrder α] [OrderTop α] {a b : α} : Disjoint (toDual a) (toDual b) ↔ Codisjoint a b :=
  Iff.rfl

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