extend_of_ind — Mathlib

English

If s is dense in α and f: s → β is uniformly continuous, then the extension of f to α agrees with f at every x ∈ s.

Русский

Если s плотно в α и f: s → β равномерно непрерывно, то продолжение f до α совпадает с f на каждом x ∈ s.

LaTeX

$$$$ \forall x\in s:\, (\text{extend}_s f)(x)=f(x). $$$$

Lean4

theorem extend_of_ind (hs : Dense s) (hf : UniformContinuous f) (x : s) : hs.extend f x = f x :=
  IsDenseInducing.extend_eq_at _ hf.continuous.continuousAt

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