IsAntichain — Mathlib

English

Let r be a relation on α and s ⊆ α. Then s is an antichain with respect to r if no two distinct elements of s are related by r.

Русский

Пусть r — отношение на α и s ⊆ α. Подмножество s называется антицепью относительно r, если любые две различные элементы из s не связаны отношением r.

LaTeX

$$$\text{IsAntichain}(r,s)$$$

Lean4

/-- An antichain is a set such that no two distinct elements are related. -/
def IsAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise rᶜ

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