extendFrom_extends — Mathlib

English

If f is continuous on A, then for every x in A, extendFrom A f x = f x.

Русский

Если f непрерывна на A, то для каждого x ∈ A верно extendFrom A f x = f x.

LaTeX

$$$$ \\forall x \\in A, \\mathrm{extendFrom}(A,f)(x) = f(x). $$$$

Lean4

theorem extendFrom_extends [T2Space Y] {f : X → Y} {A : Set X} (hf : ContinuousOn f A) :
    ∀ x ∈ A, extendFrom A f x = f x := fun x x_in ↦ extendFrom_eq (subset_closure x_in) (hf x x_in)

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