codisjoint_ofDual_iff — Mathlib

English

In the dual setting, codisjoint corresponds to disjoint via ofDual: Codisjoint (ofDual a) (ofDual b) iff Disjoint a b.

Русский

В двойственной задаче кодиссоединение сопоставляется с диссоединением через ofDual: Codisjoint (ofDual a) (ofDual b) эквивалентно Disjoint a b.

LaTeX

$$$Codisjoint (ofDual a) (ofDual b) \iff Disjoint a b$$$

Lean4

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

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