isAntichain_iff_forall_not_lt — Mathlib

English

An antichain in a preorder is equivalent to the property that no two (distinct) elements of the set satisfy a < b.

Русский

Антицепь в предупорядочении эквивалентна свойству: для любых двух элементов множества, если они оба принадлежат множеству, то не выполняется a < b.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, s) \\iff \\forall a \\in s, \\forall b \\in s, \\neg(a < b)$$$

Lean4

theorem isAntichain_iff_forall_not_lt : IsAntichain (· ≤ ·) s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ¬a < b :=
  ⟨fun hs _ ha _ => hs.not_lt ha, fun hs _ ha _ hb h h' => hs ha hb <| h'.lt_of_ne h⟩

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