antivaryOn_inv_left — Mathlib

English

Let α be a totally ordered group with IsOrderedMonoid, and β a partially ordered type. For s ⊆ ι, f : ι → α, g : ι → β, antivariation of f⁻¹ with g on s is equivalent to monovariation of f with g on s.

Русский

Пусть α — строго упорядоченная группа, обладающая структурой упорядоченного моноида, β — частично упорядоченный тип. Для s ⊆ ι функций f: ι→α, g: ι→β антивариантность f⁻¹ с g на s эквивалентна монovarияности f с g на s.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem antivaryOn_inv_left : AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s := by simp [MonovaryOn, AntivaryOn]

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