antivaryOn_inv — Mathlib

English

AntivaryOn f⁻¹ (Pi.inv g) on s is equivalent to AntivaryOn f g on s.

Русский

Антивариантность f^{-1} по отношению к g на s эквивалентна антивариантности f по отношению к g на s.

LaTeX

$$$$\\operatorname{AntivaryOn}(f^{-1}, \\operatorname{Pi.inv}(g), s) \\iff \\operatorname{AntivaryOn}(f, g, s).$$$$

Lean4

@[to_additive]
theorem antivaryOn_inv : AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s := by simp

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