IsMaxChain — Mathlib

English

A maximal chain is a chain that is not strictly contained in any larger chain.

Русский

Максимальная цепь — цепь, которая не может быть строго расширена до более крупной цепи.

LaTeX

$$$\operatorname{IsMaxChain}(r,s) \iff \operatorname{IsChain}(r,s) \land \forall t\, (\operatorname{IsChain}(r,t) \land s \subseteq t \Rightarrow s=t)$$$

Lean4

/-- A chain `s` is a maximal chain if there does not exists a chain strictly including `s`. -/
def IsMaxChain (s : Set α) : Prop :=
  IsChain r s ∧ ∀ ⦃t⦄, IsChain r t → s ⊆ t → s = t

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