mul — Mathlib

English

If hf and hf' are TendstoUniformly relations, then their product hf * hf' is TendstoUniformly.

Русский

Если hf и hf' — пределы по $l$, то hf * hf' тоже предел.

LaTeX

$$$hf \\to hf' \\Rightarrow hf * hf'\\to g*g'$$$

Lean4

@[to_additive]
theorem mul (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f * f') l s :=
  fun u hu => by simpa using (uniformContinuous_mul.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

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