monovaryOn_inv_left₀ — Mathlib

English

Let f: I → A and g: I → B with A,B linearly ordered, and s ⊆ I. If f is strictly positive on s, then MonovaryOn f^{-1} g on s is equivalent to AntivaryOn f g on s.

Русский

Пусть f: I → A и g: I → B в линейно упорядоченных множествах, возьмём подмножество s ⊆ I. Если f положительна на s, то MonovaryOn f^{-1} g on s эквивалентно AntivaryOn f g on s.

LaTeX

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

Lean4

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

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