log_pos

Mathlib.Data.Nat.Log

URI: https://scilib.ai/kg/mathlib#Nat.log_pos

English

If 1 < b and b ≤ n, then log(b, n) > 0.

Русский

Если 1 < b и b ≤ n, то log_b(n) > 0.

LaTeX

$$$1 < b \\land b \\le n \\Rightarrow 0 < \\log_b(n).$$$

Lean4

@[bound]
theorem log_pos {b n : ℕ} (hb : 1 < b) (hbn : b ≤ n) : 0 < log b n :=
  log_pos_iff.2 ⟨hbn, hb⟩

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

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

Разделы

Аффилиация

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