add_one_inj

Mathlib.SetTheory.Cardinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Cardinal.add_one_inj

English

For cardinals α,β, α + 1 = β + 1 iff α = β.

Русский

Для кардиналов α,β, α + 1 = β + 1 эквивалентно α = β.

LaTeX

$$$α + 1 = β + 1 \iff α = β$$$

Lean4

@[simp]
theorem add_one_inj {α β : Cardinal} : α + 1 = β + 1 ↔ α = β :=
  add_right_inj_of_lt_aleph0 one_lt_aleph0

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

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

Разделы

Аффилиация

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