antivary_inv_right₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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