antivary_inv_left — Mathlib

English

For f : ι → α and g : ι → β, antivariation of the inverse of f with g on a set s is equivalent to monovariation of f with g on s.

Русский

Для f: ι→α и g: ι→β антивариантность f^{-1} с g на s эквивалентна моноварияции f с g на s.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem antivary_inv_left : Antivary f⁻¹ g ↔ Monovary f g := by simp [Monovary, Antivary]

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