mul_left₀ — Mathlib

English

If hf1, hf2 are nonnegative pointwise, and h1,h2 give Monovary f g on s, then Monovary f (f1 * f2) g on s.

Русский

Пусть hf1, hf2 неотрицательны по точкам, и h1,h2 задают Monovary f g на s. Тогда Monovary f (f1 * f2) g на s.

LaTeX

$$$ (\forall i, 0 \le f_1(i)) \land (\forall i, 0 \le f_2(i)) \land Monovary f_1 g s \land Monovary f_2 g s \Rightarrow Monovary (f_1 f_2) g s $$$

Lean4

theorem mul_left₀ (hf₁ : 0 ≤ f₁) (hf₂ : 0 ≤ f₂) (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) : Monovary (f₁ * f₂) g :=
  fun _i _j hij ↦ mul_le_mul (h₁ hij) (h₂ hij) (hf₂ _) (hf₁ _)

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