monovary_inv_left₀ — Mathlib

English

If StrongLT 0 on f, then Monovary (f^{-1}) with g is equivalent to Antivary f with g.

Русский

Пусть f имеет строгую положительность около нуля, тогда Monovary(f^{-1}, g) эквивалентно Antivary(f,g).

LaTeX

$$$\\text{StrongLT }0 f \\Rightarrow \\bigl(\\text{Monovary}(f^{-1},g) \\iff \\text{Antivary}(f,g)\\bigr)$$$

Lean4

@[simp]
theorem monovary_inv_left₀ (hf : StrongLT 0 f) : Monovary f⁻¹ g ↔ Antivary f g :=
  forall₃_congr fun _i _j _ ↦ inv_le_inv₀ (hf _) (hf _)

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