div_opow_log_pos

Mathlib.SetTheory.Ordinal.Exponential

URI: https://scilib.ai/kg/mathlib#Ordinal.div_opow_log_pos

← MathLib Explorer

English

For o ≠ 0, 0 < o / (b^{log_b o}).

Русский

Если o ≠ 0, то 0 < o / (b^{log_b o}).

LaTeX

$$$ 0 < \dfrac{o}{b^{\log_b o}} $$$

Lean4

theorem div_opow_log_pos (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : 0 < o / (b ^ log b o) :=
  by
  rcases eq_zero_or_pos b with (rfl | hb)
  · simpa using Ordinal.pos_iff_ne_zero.2 ho
  · rw [div_pos (opow_ne_zero _ hb.ne')]
    exact opow_log_le_self b ho

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

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

Разделы

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

Аффилиация

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