to_dual_iff

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#IsAntichain.to_dual_iff

English

IsAntichain in α is equivalent to IsAntichain in αᵒᵈ.

Русский

Антицепочка в α эквивалентна антицепочке в αᵒᵈ.

LaTeX

$$$IsAntichain(\le) s \;\Leftrightarrow\; IsAntichain(\le)_{\alpha^{\mathrm{op}}} s$$$

Lean4

theorem to_dual_iff [LE α] : IsAntichain (· ≤ ·) s ↔ @IsAntichain αᵒᵈ (· ≤ ·) s :=
  ⟨to_dual, to_dual⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru