IsWeakAntichain — Mathlib

English

A weak antichain in Π i, α i is defined as an antichain with respect to the pointwise strict order.

Русский

Слабая антицепь в Π i, α i определяется как антицепь относительно покомпонентного строгого порядка.

LaTeX

$$$\\text{IsWeakAntichain}(s) \\coloneqq \\operatorname{IsAntichain}(\\prec, s)$$$

Lean4

/-- A weak antichain in `Π i, α i` is a set such that no two distinct elements are strongly less
than each other. -/
def IsWeakAntichain (s : Set (∀ i, α i)) : Prop :=
  IsAntichain (· ≺ ·) s

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