ofENat_mul_aleph0

Mathlib.SetTheory.Cardinal.ENat

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

← MathLib Explorer

English

If m ≠ 0, then ↑m * ℵ₀ = ℵ₀.

Русский

Если m ≠ 0, то ↑m · ℵ₀ = ℵ₀.

LaTeX

$$$\\uparrow m \\cdot \\aleph_0 = \\aleph_0 \\quad \\text{при } m \\neq 0$$$

Lean4

@[simp]
theorem ofENat_mul_aleph0 {m : ℕ∞} (hm : m ≠ 0) : ↑m * ℵ₀ = ℵ₀ := by
  induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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