uniformly_extend_spec — Mathlib

English

If uniform continuity holds on a subtype, and the embedding is dense, then a uniform extension exists with a limit c.

Русский

Если для подмножества задана равномерно непрерывная часть, а вложение плотное, то существует равномерное продолжение с пределом c.

LaTeX

$$$\exists c, \text{ Tendsto } (f|_{\text{Subtype}}) \text{ to } c.$$$

Lean4

theorem uniformly_extend_spec [CompleteSpace γ] (a : α) : Tendsto f (comap e (𝓝 a)) (𝓝 (ψ a)) := by
  simpa only [IsDenseInducing.extend] using tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)

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