add_nat_eq — Mathlib

English

For every infinite cardinal a (i.e., a ≥ ℵ0) and every natural n, a + n = a.

Русский

Для каждого бесконечного кардинала a (то есть a ≥ ℵ0) и любого натурального числа n выполняется a + n = a.

LaTeX

$$$\forall a\, \forall n \in \mathbb{N},\ \aleph_0 \le a \Rightarrow a + n = a$$$

Lean4

theorem add_nat_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : a + n = a :=
  add_eq_left ha ((nat_lt_aleph0 _).le.trans ha)

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