add_right_inj_of_lt_aleph0 — Mathlib

English

For cardinals α,β,γ with γ < aleph0, adding γ on the right is injective: α + γ = β + γ implies α = β.

Русский

Для кардиналов α,β,γ с γ < ℵ0, добавление γ справа инъективно: α + γ = β + γ ⇒ α = β.

LaTeX

$$$\forall α,β,γ\, (\gamma < \aleph_0) \Rightarrow (α + γ = β + γ) \Rightarrow α = β$$$

Lean4

theorem add_right_inj_of_lt_aleph0 {α β γ : Cardinal} (γ₀ : γ < aleph0) : α + γ = β + γ ↔ α = β :=
  ⟨fun h => Cardinal.eq_of_add_eq_add_right h γ₀, fun h => congr_arg (· + γ) h⟩

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