mul_left — Mathlib

English

If f1 and f2 are monovary with g, then their product is monovary with g.

Русский

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

LaTeX

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

Lean4

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

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