power_nat_le_max — Mathlib

English

For any cardinals c and natural n, c^{n} ≤ max(c, ℵ0).

Русский

Для любых кардиналов c и натурального n выполняется c^{n} ≤ max(c, ℵ0).

LaTeX

$$$ c^{n} \\le \\max(c, \\aleph_0) $$$

Lean4

theorem power_nat_le_max {c : Cardinal.{u}} {n : ℕ} : c ^ (n : Cardinal.{u}) ≤ max c ℵ₀ :=
  by
  rcases le_or_gt ℵ₀ c with hc | hc
  · exact le_max_of_le_left (power_nat_le hc)
  · exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le

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