log_lt_log

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#WithZero.log_lt_log

← MathLib Explorer

English

If x ≠ 0 and y ≠ 0, then log x < log y iff x < y.

Русский

Если x ≠ 0 и y ≠ 0, то log x < log y эквивалентно x < y.

LaTeX

$$$(x \neq 0) \land (y \neq 0) \Rightarrow \log x < \log y \iff x < y$$$

Lean4

@[simp]
theorem log_lt_log (hx : x ≠ 0) (hy : y ≠ 0) : log x < log y ↔ x < y := by lift x to Multiplicative G using hx;
  lift y to Multiplicative G using hy; simp [log]

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

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

Разделы

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

Аффилиация

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