IsChain — Mathlib

English

A chain is a set in which any two distinct elements are comparable by the relation.

Русский

Цепь — множество, в котором любые два различных элемента сравнимы по отношению.

LaTeX

$$$\forall x\in S\,\forall y\in S\,(x \neq y \rightarrow (r\,x\,y) \lor (r\,y\,x))$$$

Lean4

/-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
def IsChain (s : Set α) : Prop :=
  s.Pairwise fun x y => x ≺ y ∨ y ≺ x

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