inseparable_extend_coe — Mathlib

English

For a complete Hausdorff space, the extended map preserves the value on image points: (pkg.extend f)(ι a) = f a for all a.

Русский

При полной (T2-) пространстве расширенная функция сохраняет значения на образах: (pkg.extend f)(ι a) = f a для всех a.

LaTeX

$$$\\forall a, (pkg.extend f)(\\iota(a)) = f(a)$$$

Lean4

theorem inseparable_extend_coe (hf : UniformContinuous f) (x : α) : Inseparable (pkg.extend f (ι x)) (f x) :=
  by
  rw [extend_def _ hf]
  exact pkg.isDenseInducing.inseparable_extend hf.continuous.continuousAt

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