extend_eq_at — Mathlib

English

If the domain α is separable and e : α → β is a dense embedding, then β is separable as well.

Русский

Если область α сепарируемая и e : α → β плотное вложение, то β тоже сепарабелен.

LaTeX

$$$SeparableSpace\\alpha \\Rightarrow (IsDenseEmbedding e) \\rightarrow SeparableSpace \\beta$$$

Lean4

theorem extend_eq_at [T2Space β] (hs : Dense s) {f : s → β} {x : s} (hf : ContinuousAt f x) : hs.extend f x = f x :=
  hs.isDenseInducing_val.extend_eq_at hf

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