range_mul — Mathlib

English

If the ranges of f and g are bounded below, then the range of f(i) g(i) is bounded below.

Русский

Если диапазоны функций f и g ограничены снизу, то диапазон их покомпонентного произведения ограничен снизу.

LaTeX

$$BddBelow (range f) \rightarrow BddBelow (range g) \Rightarrow BddBelow (range (\lambda i, f i * g i))$$

Lean4

@[to_additive]
theorem range_mul (hf : BddBelow (range f)) (hg : BddBelow (range g)) : BddBelow (range fun i ↦ f i * g i) :=
  BddAbove.range_mul (M := Mᵒᵈ) hf hg

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