aleph0_mul_nat

Mathlib.SetTheory.Cardinal.Basic

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

English

For any natural n with n ≠ 0, ℵ₀ · n = ℵ₀.

Русский

Для любого натурального n ≠ 0 ℵ₀ · n = ℵ₀.

LaTeX

$$$ \aleph_0 \cdot n = \aleph_0 \quad\text{for } n \neq 0$$$

Lean4

@[simp]
theorem aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) : ℵ₀ * n = ℵ₀ := by rw [mul_comm, nat_mul_aleph0 hn]

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

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

Разделы

Аффилиация

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