mod_opow_log_lt_self

Mathlib.SetTheory.Ordinal.Exponential

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

← MathLib Explorer

English

For any base b and o ≠ 0, o mod (b^{log_b o}) < o.

Русский

Для любой основы b и o ≠ 0: o mod (b^{log_b o}) < o.

LaTeX

$$$ o \% (b^{\log_b o}) < o $$$

Lean4

theorem mod_opow_log_lt_self (b : Ordinal) {o : Ordinal} (ho : o ≠ 0) : o % (b ^ log b o) < o :=
  by
  rcases eq_or_ne b 0 with (rfl | hb)
  · simpa using Ordinal.pos_iff_ne_zero.2 ho
  · exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)

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

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

Разделы

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

Аффилиация

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