veblen_injective

Mathlib.SetTheory.Ordinal.Veblen

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

English

For every ordinal o, the function a ↦ veblen(o,a) is injective.

Русский

Для каждого ординала o функция a ↦ veblen(o,a) инъективна.

LaTeX

$$$$\\forall a,b\\, (\\operatorname{veblen}(o,a) = \\operatorname{veblen}(o,b) \\Rightarrow a=b).$$$$

Lean4

theorem veblen_injective (o : Ordinal) : Function.Injective (veblen o) :=
  veblenWith_injective (isNormal_opow one_lt_omega0) o

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

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

Разделы

Аффилиация

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