nat_add_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

Let a be a cardinal with a ≥ ℵ0 and n ∈ ℕ. Then n + a = a.

Русский

Пусть a — кардинал с a ≥ ℵ0 и n ∈ ℕ. Тогда n + a = a.

LaTeX

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

Lean4

theorem nat_add_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : n + a = a := by rw [add_comm, add_nat_eq n ha]

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

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

Разделы

Аффилиация

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