div — Mathlib

English

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

Русский

Если hf и hf' — пределы равномерности по $l$ и $l'$, то их произведение hf * hf' тоже предел равномерности.

LaTeX

$$$hf \\; hf' \\Rightarrow hf * hf'$$$

Lean4

@[to_additive]
theorem div (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f / f') (g / g') l :=
  fun u hu => ((uniformContinuous_div.comp_tendstoUniformly (hf.prodMk hf')) u hu).diag_of_prod

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