monovaryOn_inv_right₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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