power_eq_two_power — Mathlib

English

Let c1 and c2 be cardinals with ℵ0 ≤ c1, 2 ≤ c2, and c2 ≤ c1. Then c2^{c1} = 2^{c1}.

Русский

Пусть c1 и c2 — кардиналы, удовлетворяющие ℵ0 ≤ c1, 2 ≤ c2 и c2 ≤ c1. Тогда c2^{c1} = 2^{c1}.

LaTeX

$$$ (\\aleph_0 \\le c_1) \\land (2 \\le c_2) \\land (c_2 \\le c_1) \\implies c_2^{c_1} = 2^{c_1} $$$

Lean4

theorem power_eq_two_power {c₁ c₂ : Cardinal} (h₁ : ℵ₀ ≤ c₁) (h₂ : 2 ≤ c₂) (h₂' : c₂ ≤ c₁) : c₂ ^ c₁ = 2 ^ c₁ :=
  le_antisymm (power_self_eq h₁ ▸ power_le_power_right h₂') (power_le_power_right h₂)

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