nat_mul_continuum

Mathlib.SetTheory.Cardinal.Continuum

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

← MathLib Explorer

English

For any natural n ≠ 0, n * 𝔠 = 𝔠.

Русский

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

LaTeX

$$$\text{For all } n \neq 0:\; n \cdot \mathfrak{c} = \mathfrak{c}$$$

Lean4

@[simp]
theorem nat_mul_continuum {n : ℕ} (hn : n ≠ 0) : ↑n * 𝔠 = 𝔠 :=
  mul_eq_right aleph0_le_continuum (nat_lt_continuum n).le (Nat.cast_ne_zero.2 hn)

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

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

Разделы

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

Аффилиация

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