antivary_inv₀ — Mathlib

English

If f and g are strictly positive with strong LT, antivary of inverses equals antivary of originals.

Русский

Если f и g строго положительны и имеют StrongLT, antivary инверсий равно antivary исходных функций.

LaTeX

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

Lean4

theorem antivary_inv₀ (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Antivary f⁻¹ g⁻¹ ↔ Antivary f g := by
  rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]

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