antivaryOn_inv₀ — Mathlib

English

If f is positively valued and g is positively valued, antivary-on with inverses equals antivary-on with originals.

Русский

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

LaTeX

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

Lean4

theorem antivaryOn_inv₀ (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s := by
  rw [antivaryOn_inv_left₀ hf, monovaryOn_inv_right₀ hg]

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