comp_familyOfBFamily' — Mathlib

English

The range of a higher-universe-valued ordinal function is bounded above.

Русский

Диапазон функции, возвращающей значения в большем универсуме, ограничен сверху.

LaTeX

$$$\exists M\in\text{Ord},\ \forall x\in \mathrm{range}(f),\ x \le M$$$

Lean4

theorem comp_familyOfBFamily' {ι : Type u} (r : ι → ι → Prop) [IsWellOrder ι r] {o} (ho : type r = o) (f : ∀ a < o, α)
    (g : α → β) : g ∘ familyOfBFamily' r ho f = familyOfBFamily' r ho fun i hi => g (f i hi) :=
  rfl

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