antivaryOn_inv_right₀ — Mathlib

English

If g is strictly positive on s, AntivaryOn f with g^{-1} on s is equivalent to MonovaryOn f with g on s.

Русский

Если g положительна на s, AntivaryOn f с g^{-1} на s эквивалентно MonovaryOn f с g на s.

LaTeX

$$$\\left(\\forall i \\in s,\\ 0 < g(i)\\right) \\Rightarrow \\bigl(\\text{AntivaryOn}(f,g^{-1},s) \\iff \\text{MonovaryOn}(f,g,s)\\bigr)$$$

Lean4

@[simp]
theorem antivaryOn_inv_right₀ (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s :=
  forall₂_swap.trans <| forall₄_congr fun i hi j hj ↦ by simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

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