veblen_zero_inj

Mathlib.SetTheory.Ordinal.Veblen

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

English

For all o1, o2, veblen(o1,0) = veblen(o2,0) implies o1 = o2.

Русский

Для всех o1, o2, если veblen(o1,0) = veblen(o2,0), то o1 = o2.

LaTeX

$$$$\\operatorname{veblen}(o_1,0) = \\operatorname{veblen}(o_2,0) \\iff o_1 = o_2.$$$$

Lean4

@[simp]
theorem veblen_zero_inj : veblen o₁ 0 = veblen o₂ 0 ↔ o₁ = o₂ :=
  veblen_zero_strictMono.injective.eq_iff

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

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

Разделы

Аффилиация

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