gamma_inj

Mathlib.SetTheory.Ordinal.Veblen

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

English

Γ is injective: Γ_a = Γ_b iff a = b.

Русский

Γ инъективна: Γ_a = Γ_b ⇔ a = b.

LaTeX

$$$\\Gamma_a = \\Gamma_b \iff a = b$$$

Lean4

@[simp]
theorem gamma_inj : Γ_ a = Γ_ b ↔ a = b :=
  strictMono_gamma.injective.eq_iff

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

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

Разделы

Аффилиация

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