mul_left — Mathlib

English

If f1 and f2 antivary with g on s, then their product antivaries with g on s.

Русский

Если f1 и f2 антивариантно варьируются с g на s, то их произведение антивариантно варьируется с g на s.

LaTeX

$$$$\\operatorname{AntivaryOn}(f_1, g, s) \\land \\operatorname{AntivaryOn}(f_2, g, s) \\Rightarrow \\operatorname{AntivaryOn}(f_1 f_2, g, s).$$$$

Lean4

@[to_additive]
theorem mul_left (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) : Antivary (f₁ * f₂) g := fun _i _j hij ↦
  mul_le_mul' (h₁ hij) (h₂ hij)

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