monovary_inv_left — Mathlib

English

For f : ι → α and g : ι → β with α a commutative ordered group and IsOrderedMonoid, the monovariation of the inverse of f with g is equivalent to the antivariation of f with g.

Русский

Пусть f: ι→α, g: ι→β и α — коммутативная упорядоченная группа с IsOrderedMonoid; моноварьированность f^{-1} с g эквивалентна антивариантности f с g.

LaTeX

$$$$\\operatorname{Monovary}(f^{-1}, g) \\iff \\operatorname{Antivary}(f, g).$$$$

Lean4

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

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