extend_eq — Mathlib

English

Let i : α → β be a dense inducing map between topological spaces and let f : α → γ be continuous. Then the extension extend f : β → γ satisfies (extend f)(i(a)) = f(a) for every a ∈ α.

Русский

Пусть i : α → β — плотное индуцирующее отображение между топологическими пространствами и пусть f : α → γ непрерывно. Тогда продолжение extend f : β → γ удовлетворяет (extend f)(i(a)) = f(a) для каждого a ∈ α.

LaTeX

$$$\\\\forall a \\\\in \u03b1, \\\\(\\\\operatorname{extend} f)(i(a)) = f(a) \\\\;,$$$

Lean4

theorem extend_eq [T2Space γ] (di : IsDenseInducing i) {f : α → γ} (hf : Continuous f) (a : α) :
    di.extend f (i a) = f a :=
  di.extend_eq_at hf.continuousAt

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