pow_le — Mathlib

English

Let κ ≥ ℵ0 and μ < ℵ0. Then κ^μ ≤ κ.

Русский

Пусть κ ≥ ℵ0 и μ < ℵ0. Тогда κ^μ ≤ κ.

LaTeX

$$$\aleph_0 \le κ \quad\text{и}\quad μ < \aleph_0 \Rightarrow κ^μ \le κ$$$

Lean4

theorem pow_le {κ μ : Cardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : μ < ℵ₀) : κ ^ μ ≤ κ :=
  let ⟨n, H3⟩ := lt_aleph0.1 H2
  H3.symm ▸
    Quotient.inductionOn κ
      (fun α H1 =>
        Nat.recOn n
          (lt_of_lt_of_le
              (by
                rw [Nat.cast_zero, power_zero]
                exact one_lt_aleph0)
              H1).le
          fun n ih =>
          le_of_le_of_eq
            (by
              rw [Nat.cast_succ, power_add, power_one]
              exact mul_le_mul_right' ih _)
            (mul_eq_self H1))
      H1

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