isAntichain — Mathlib

English

If A is a family of Finset α whose elements all have size r, then A is an antichain with respect to inclusion: for any s,t ∈ A, if s ⊆ t then s = t.

Русский

Если A — семейство Finset α, элементы которого все имеют размер r, то A является антицепочкой относительно включения: для любых s,t ∈ A, если s ⊆ t, то s = t.

LaTeX

$$$ A.Sized r \Rightarrow IsAntichain(\subseteq) A $$$

Lean4

protected theorem isAntichain (hA : A.Sized r) : IsAntichain (· ⊆ ·) A := fun _s hs _t ht h hst =>
  h <| Finset.eq_of_subset_of_card_le hst ((hA ht).trans (hA hs).symm).le

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