clog_pos

Mathlib.Data.Nat.Log

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

English

If hb: 1 < b and hn: 2 ≤ n, then 0 < clog_b(n).

Русский

Если hb: 1 < b и hn: 2 ≤ n, то 0 < clog_b(n).

LaTeX

$$$ (1 < b) \land (2 \le n) \Rightarrow 0 < \operatorname{clog}(b,n) $$$

Lean4

theorem clog_pos {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : 0 < clog b n :=
  by
  rw [clog_of_two_le hb hn]
  exact zero_lt_succ _

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

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

Разделы

Аффилиация

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