power_nat_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

If ℵ0 ≤ c and n ≥ 1, then c^{n} = c.

Русский

Если ℵ0 ≤ c и n ≥ 1, то c^{n} = c.

LaTeX

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

Lean4

theorem power_nat_eq {c : Cardinal.{u}} {n : ℕ} (h1 : ℵ₀ ≤ c) (h2 : 1 ≤ n) : c ^ n = c :=
  pow_eq h1 (mod_cast h2) (nat_lt_aleph0 n)

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

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

Разделы

Аффилиация

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