add_nat_inj

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For cardinals α,β and n ∈ ℕ, α + n = β + n iff α = β.

Русский

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

LaTeX

$$$\forall α,β \in \mathrm{Cardinal},\forall n \in \mathbb{N},\ (α + n = β + n) \iff (α = β)$$$

Lean4

@[simp]
theorem add_nat_inj {α β : Cardinal} (n : ℕ) : α + n = β + n ↔ α = β :=
  add_right_inj_of_lt_aleph0 (nat_lt_aleph0 _)

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

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

Разделы

Аффилиация

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