log_injective

Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

URI: https://scilib.ai/kg/mathlib#ENNReal.log_injective

English

The logarithm on ENNReal is injective: log x = log y implies x = y.

Русский

Логарифм на ENNReal инъективен: log x = log y ⇒ x = y.

LaTeX

$$log x = log y \Rightarrow x = y$$

Lean4

theorem log_injective : Function.Injective log :=
  log_strictMono.injective

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

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

Разделы

Аффилиация

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