extend_eq — Mathlib

English

For a dense subset s and a continuous f : s → β, the extension satisfies (extend f)(x) = f(x) for x ∈ s.

Русский

Для плотной подзадачи s и непрерывной функции f : s → β продолжение удовлетворяет (extend f)(x) = f(x) для x ∈ s.

LaTeX

$$$\\\\forall x \\in s, \\\\(\\\\operatorname{extend} f)(x) = f(x)$$$

Lean4

theorem extend_eq [T2Space β] (hs : Dense s) (hf : Continuous f) (x : s) : hs.extend f x = f x :=
  hs.extend_eq_at hf.continuousAt

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