inv

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#StrictAnti.inv

English

If f is strictly decreasing, then x ↦ f(x)^{-1} is strictly increasing.

Русский

Если f строго убывающая, то x ↦ f(x)^{-1} строго возрастает.

LaTeX

$$$ \text{StrictAnti}(f) \Rightarrow \text{StrictMono}(x \mapsto f(x)^{-1}). $$$

Lean4

@[to_additive]
theorem inv (hf : StrictAnti f) : StrictMono fun x => (f x)⁻¹ := fun _ _ hxy => inv_lt_inv_iff.2 (hf hxy)

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

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

Разделы

Аффилиация

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