monovary_inv_right₀ — Mathlib

English

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

Русский

Пусть StrongLT 0 на g. Тогда Monovary f с g^{-1} эквивалентно Antivary f с g.

LaTeX

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

Lean4

@[simp]
theorem monovary_inv_right₀ (hg : StrongLT 0 g) : Monovary f g⁻¹ ↔ Antivary f g :=
  forall_swap.trans <| forall₂_congr fun i j ↦ by simp [inv_lt_inv₀ (hg _) (hg _)]

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