isWeakAntichain — Mathlib

English

If a set s is an antichain with respect to the pointwise order, then s is a weak antichain.

Русский

Если множество s является антицепью относительно покомпонентным порядком, то оно является слабой антицепью.

LaTeX

$$$\mathrm{IsAntichain}(s) \Rightarrow \mathrm{IsWeakAntichain}(s)$$$

Lean4

protected theorem isWeakAntichain (hs : IsAntichain (· ≤ ·) s) : IsWeakAntichain s :=
  hs.mono fun _ _ => le_of_strongLT

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