power_aleph0_of_le_continuum

Mathlib.SetTheory.Cardinal.Continuum

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

← MathLib Explorer

English

If 2 ≤ x ≤ 𝔠 then x^ℵ₀ = 𝔠.

Русский

Если 2 ≤ x ≤ 𝔠, то x^ℵ₀ = 𝔠.

LaTeX

$$$2 \le x \le \mathfrak{c} \;\Rightarrow\; x^{\aleph_0} = \mathfrak{c}$$$

Lean4

theorem power_aleph0_of_le_continuum {x : Cardinal} (h₁ : 2 ≤ x) (h₂ : x ≤ 𝔠) : x ^ ℵ₀ = 𝔠 :=
  by
  apply le_antisymm
  · rw [← continuum_power_aleph0]
    exact power_le_power_right h₂
  · rw [← two_power_aleph0]
    exact power_le_power_right h₁

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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