IsStrongAntichain — Mathlib

English

For any predicate P, the set {x | Minimal P x} is an antichain with respect to ≤.

Русский

Для произвольного предиката P множество {x | Minimal P x} является антицепочкой относительно ≤.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, \\{x \\mid \\operatorname{Minimal} P x\\})$$$

Lean4

/-- A strong (upward) antichain is a set such that no two distinct elements are related to a common
element. -/
def IsStrongAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise fun a b => ∀ c, ¬r a c ∨ ¬r b c

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