cantor'

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.cantor'

← MathLib Explorer

English

Cantor’s theorem variant: for all a and b with b > 1, a < b^a.

Русский

Вариант теоремы Кантора: для любых a и b, если b > 1, то a < b^a.

LaTeX

$$$\forall a \in \mathrm{Cardinal},\ \forall b > 1:\ a < b^a$$$

Lean4

theorem cantor' (a) {b : Cardinal} (hb : 1 < b) : a < b ^ a :=
  by
  rw [← succ_le_iff, (by norm_cast : succ (1 : Cardinal) = 2)] at hb
  exact (cantor a).trans_le (power_le_power_right hb)

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

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

Разделы

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

Аффилиация

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