div — Mathlib

English

If f and f' are UniformCauchySeqOn on l with respect to s, then f/f' is UniformCauchySeqOn on l with respect to s.

Русский

Если f и f' — равномерно Коши на множестве s и языке l, то f/f' тоже равномерно Коши.

LaTeX

$$$\\mathrm{UniformCauchySeqOn}\\ f\\ l\\ s \\Rightarrow \\mathrm{UniformCauchySeqOn}\\ f' l s \\Rightarrow \\mathrm{UniformCauchySeqOn}\\ (f / f')\\ l\\ s$$$

Lean4

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

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