to_dual — Mathlib

English

If s is an antichain in α with respect to ≤, then it is an antichain in the dual order αᵒᵈ.

Русский

Если s является антицепочкой в α относительно ≤, то она остается антицепочкой в двойственном порядке αᵒᵈ.

LaTeX

$$$IsAntichain(≤)_{\alpha^{\mathrm{op}}}(s)$$$

Lean4

theorem to_dual [LE α] (hs : IsAntichain (· ≤ ·) s) : @IsAntichain αᵒᵈ (· ≤ ·) s := fun _ ha _ hb hab =>
  hs hb ha hab.symm

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