extend_pureCauchy — Mathlib

English

For f: α → β with hf UniformContinuous, extend f agrees with f on pureCauchy a.

Русский

Для f: α → β с hf UniformContinuous продолжение extend f совпадает с f на pureCauchy a.

LaTeX

$$$\\text{extend}_{f}(\\mathrm{pureCauchy}(a))=f(a) \\quad(\\forall a)$$$

Lean4

theorem extend_pureCauchy {f : α → β} (hf : UniformContinuous f) (a : α) : extend f (pureCauchy a) = f a :=
  by
  rw [extend, if_pos hf]
  exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

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