continuousAt_extend — Mathlib

English

For a dense inducing i: α → β and a tail condition hf, the extended map is continuous at a.

Русский

Для плотного индуцирующего отображения i: α → β и условия hf продолжение непрерывно в точке a.

LaTeX

$$$[T3Space γ] \\\\Rightarrow \\\\; \\\\text{ContinuousAt} (\\\\mathrm{extend} f) a \\\\text{ under } hf$$$

Lean4

theorem continuousAt_extend [T3Space β] {a : α} (hs : Dense s)
    (hf : ∀ᶠ x in 𝓝 a, ∃ b, Tendsto f (comap (↑) <| 𝓝 x) (𝓝 b)) : ContinuousAt (hs.extend f) a :=
  hs.isDenseInducing_val.continuousAt_extend hf

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