pow_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

If κ ≥ ℵ0, μ ≥ 1 and μ < ℵ0, then κ^μ = κ.

Русский

Если κ ≥ ℵ0, 1 ≤ μ < ℵ0, то κ^μ = κ.

LaTeX

$$$κ \ge \aleph_0,\ 1 \le μ,\ μ < \aleph_0 \Rightarrow κ^μ = κ$$$

Lean4

theorem pow_eq {κ μ : Cardinal.{u}} (H1 : ℵ₀ ≤ κ) (H2 : 1 ≤ μ) (H3 : μ < ℵ₀) : κ ^ μ = κ :=
  (pow_le H1 H3).antisymm <| self_le_power κ H2

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

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

Разделы

Аффилиация

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