contained — Mathlib

English

Define for an ordinal o the predicate that C is contained in all i with ord I i < o.

Русский

Определим для ординала o предикат: C содержится во всех i с ord I i < o.

LaTeX

$$$\\mathrm{contained}(o) := \\forall f\\in C, \\forall i, f(i)=\\mathrm{true} \\Rightarrow \\mathrm{ord}_I(i) < o.$$$

Lean4

/-- A predicate saying that `C` is "small" enough to satisfy the inductive hypothesis. -/
def contained (o : Ordinal) : Prop :=
  ∀ f, f ∈ C → ∀ (i : I), f i = true → ord I i < o

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