antivaryOn_inv_left₀ — Mathlib

English

Let hf: ∀ i ∈ s, 0 < f i. Then AntivaryOn f^{-1} g on s is equivalent to MonovaryOn f g on s.

Русский

Пусть hf: ∀ i ∈ s, 0 < f i. Тогда AntivaryOn f^{-1} g на s эквивалентно MonovaryOn f g на s.

LaTeX

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

Lean4

@[simp]
theorem antivaryOn_inv_left₀ (hf : ∀ i ∈ s, 0 < f i) : AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s :=
  forall₅_congr fun _i hi _j hj _ ↦ inv_le_inv₀ (hf _ hj) (hf _ hi)

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