logb_nonneg_iff

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#Real.logb_nonneg_iff

English

For 1 < b and hx > 0, log_b x ≥ 0 if and only if x ≥ 1.

Русский

Для 1 < b и hx > 0: log_b x ≥ 0 тогда x ≥ 1.

LaTeX

$$$1 < b \land x > 0 \Rightarrow \log_b x \ge 0 \iff x \ge 1.$$$

Lean4

theorem logb_nonneg_iff (hx : 0 < x) : 0 ≤ logb b x ↔ 1 ≤ x := by rw [← not_lt, logb_neg_iff hb hx, not_lt]

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

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

Разделы

Аффилиация

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