mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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