mul_right — Mathlib

English

If f antivaries with g1 and with g2 on s, then f antivaries with g1·g2 on s.

Русский

Если f антивариантна по отношению к g1 и по отношению к 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₁ : Antivary f g₁) (h₂ : Antivary f g₂) : Antivary f (g₁ * g₂) := fun _i _j hij ↦
  (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

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