English
Under suitable hypotheses, there exists an extended limit c in γ for a uniformly continuous function f defined on a subtype, matching e-structure.
Русский
При надлежащих условиях существует предел c в γ для равномерно непрерывной функции f, определённой на подпространстве, совместимый с структурой e.
LaTeX
$$$\exists c, \text{ Tendsto } f\; (\text{comap } e \; (\nhds b)) \ (\nhds c)\; \text{ under the given hypotheses.}$$$
Lean4
theorem uniformly_extend_exists [CompleteSpace γ] (a : α) : ∃ c, Tendsto f (comap e (𝓝 a)) (𝓝 c) :=
let de := h_e.isDenseInducing h_dense
have : Cauchy (𝓝 a) := cauchy_nhds
have : Cauchy (comap e (𝓝 a)) := this.comap' (le_of_eq h_e.comap_uniformity) (de.comap_nhds_neBot _)
have : Cauchy (map f (comap e (𝓝 a))) := this.map h_f
CompleteSpace.complete this
