English
Let f : ι → α and g1, g2 : ι → β be functions with α a partially ordered set and β a totally ordered multiplicative group-like structure. If f antivaries with g1 on a set s and f antivaries with g2 on s, then f antivaries with the product g1 · g2 on s.
Русский
Пусть f: ι → α и g1, g2: ι → β — функции. Пусть α упорядчено частично, β — упорядкована по лево-моной структуре. Если f антивариантна по отношению к g1 на s и антивариантна по отношению к g2 на s, то f антивариантна по отношению к произведению g1 · g2 на s.
LaTeX
$$$ AntivaryOn f g_1 s \land AntivaryOn f g_2 s \Rightarrow AntivaryOn f (g_1 g_2) s $$$
Lean4
@[to_additive]
theorem mul_right (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : AntivaryOn f (g₁ * g₂) s := fun _i hi _j hj hij ↦
(lt_or_lt_of_mul_lt_mul hij).elim (h₁ hi hj) <| h₂ hi hj
