continuous_extend_of_cauchy — Mathlib

English

Let e: α → β be a dense inducing map and suppose that for every b ∈ β the image under f along comap e of nhds b is Cauchy; then the extension of f along e is continuous.

Русский

Пусть e: α → β — плотное индуктивное отображение; если для каждого b ∈ β отображение f через comap e и nhds b является Коши, то продолжение f по e непрерывно.

LaTeX

$$$\\text{If } e:\\alpha\\to\\beta \\text{ is dense inducing and }\\forall b\\, (Cauchy\\, (map\\ f\\ (comap\\ e\\ (\\mathcal{N}_b)))),\\ then\\ Continuous(\\mathrm{extend}_e f).$$$

Lean4

theorem continuous_extend_of_cauchy {e : α → β} {f : α → γ} (de : IsDenseInducing e)
    (h : ∀ b : β, Cauchy (map f (comap e <| 𝓝 b))) : Continuous (de.extend f) :=
  de.continuous_extend fun b => CompleteSpace.complete (h b)

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