maxChain — Mathlib

English

maxChain r is the union of all sets in the ChainClosure r, i.e., the explicit maximal chain built from r by taking the union of all chains.

Русский

maxChain r есть объединение всех множеств в ChainClosure r, то есть явно заданная максимальная цепь, строимая из r.

LaTeX

$$$ \text{maxChain}(r) = \bigcup\limits_{C \in \text{ChainClosure}(r)} C.$$$

Lean4

/-- An explicit maximal chain. `maxChain` is taken to be the union of all sets in `ChainClosure`. -/
def maxChain (r : α → α → Prop) : Set α :=
  ⋃₀ setOf (ChainClosure r)

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