veblen_mem_range_opow — Mathlib

English

For any o,a, veblen o a lies in the range of the map x ↦ ω^x.

Русский

Для любых o,a значение veblen o a лежит в диапазоне отображения x ↦ ω^x.

LaTeX

$$$\forall o,a:\operatorname{Ordinal},\ \operatorname{veblen}(o,a) \in \operatorname{range}(\omega^{\cdot})$$$

Lean4

theorem veblen_mem_range_opow (o a : Ordinal) : veblen o a ∈ range (ω ^ · : Ordinal → Ordinal) :=
  veblenWith_mem_range (isNormal_opow one_lt_omega0)

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