range_mul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) : BddAbove (range fun i ↦ f i * g i) :=
  .range_comp (f := fun i ↦ (f i, g i)) (bddAbove_range_prod.2 ⟨hf, hg⟩) (monotone_fst.mul' monotone_snd)

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