mem_range_gamma

Mathlib.SetTheory.Ordinal.Veblen

URI: https://scilib.ai/kg/mathlib#Ordinal.mem_range_gamma

English

An ordinal o lies in the range of Γ if and only if the 0-th Veblen function fixes o, i.e., veblen(o,0) = o.

Русский

Некая ординальная величина o принадлежит диапазону Γ тогда и только тогда, когда veblen(o, 0) = o.

LaTeX

$$$o \in \mathrm{range}(\\Gamma_) \iff \\veblen(o,0) = o$$$

Lean4

theorem mem_range_gamma : o ∈ range Γ_ ↔ veblen o 0 = o :=
  isNormal_veblen_zero.mem_range_deriv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru