English
Let α be a totally ordered commutative group with IsOrderedMonoid structure and β a partially ordered type. For any s ⊆ ι and f : ι → α, g : ι → β, the monovariation of the inverse of f with g on s is equivalent to the antivariation of f with g on s.
Русский
Пусть α — совершенно упорядоченная коммутативная группа, обладающая структурой упорядкованного моноида, и β — частично упорядченный тип.Для любого подмножества s ⊆ ι и функций f: ι→α, g: ι→β моно-варьированность f⁻¹ и g на s эквивалентна антивариантности f и g на s.
LaTeX
$$$$\\operatorname{MonovaryOn}(f^{-1}, g, s) \\iff \\operatorname{AntivaryOn}(f, g, s)$$$$
Lean4
@[to_additive (attr := simp)]
theorem monovaryOn_inv_left : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s := by simp [MonovaryOn, AntivaryOn]
