monovary_inv₀ — Mathlib

English

If f and g are strictly positive, then Monovary f^{-1} g^{-1} is equivalent to Monovary f g, provided both f and g are strongly LT at 0.

Русский

Если f и g строго положительны, то Monovary f^{-1} g^{-1} эквивалентна Monovary f g при условии StrongLT 0 внутри.

LaTeX

$$$\\text{StrongLT }0 f \\land \\text{StrongLT }0 g \\Rightarrow \\bigl(\\text{Monovary}(f^{-1},g^{-1}) \\iff \\text{Monovary}(f,g)\\bigr)$$$

Lean4

theorem monovary_inv₀ (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Monovary f⁻¹ g⁻¹ ↔ Monovary f g := by
  rw [monovary_inv_left₀ hf, antivary_inv_right₀ hg]

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