subchain — Mathlib

English

The subchain of a Set α is the set of lists that are strictly increasing and whose elements lie in that set.

Русский

Подцепь множества α состоит из списков, которые строго возрастают и элементы которых принадлежат этому множеству.

LaTeX

$$$ \\mathrm{subchain}(s) = \\{\, l \\mid l \\text{ is strictly increasing under } < \\text{ and } \\forall i \\in l,\, i \\in s \\,\\}$$$

Lean4

/-- The set of strictly ascending lists of `α` contained in a `Set α`. -/
def subchain : Set (List α) :=
  {l | l.IsChain (· < ·) ∧ ∀ i ∈ l, i ∈ s}

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