monovaryOn_inv₀ — Mathlib

English

If f and g are both strictly positive, then Monovary of their inverses is equivalent to Monovary of the originals.

Русский

Если f и g строго положительны, то моновариантность их обращённых функций эквивалентна моновариантности самих функций.

LaTeX

$$$\\forall f,g\\ (\\text{hf},\\text{hg} \\text{ StrictPos})\\; \\text{Monovary}(f^{-1},g^{-1}) \\iff \\text{Monovary}(f,g)$$$

Lean4

theorem monovaryOn_inv₀ (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s := by
  rw [monovaryOn_inv_left₀ hf, antivaryOn_inv_right₀ hg]

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