nat_power_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

← MathLib Explorer

English

If c is infinite (ℵ0 ≤ c) and n ≥ 2, then (n)^{c} = 2^{c}.

Русский

Если c бесконечен (ℵ0 ≤ c) и n ≥ 2, то n^{c} = 2^{c}.

LaTeX

$$$ (\\aleph_0 \\le c) \\land (2 \\le n) \\implies n^{c} = 2^{c} $$$

Lean4

theorem nat_power_eq {c : Cardinal.{u}} (h : ℵ₀ ≤ c) {n : ℕ} (hn : 2 ≤ n) : (n : Cardinal.{u}) ^ c = 2 ^ c :=
  power_eq_two_power h (by assumption_mod_cast) ((nat_lt_aleph0 n).le.trans h)

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

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

Разделы

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

Аффилиация

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