extend_unique — Mathlib

English

Let hs be a dense subset. If for all x ∈ α, g(i x) = f x and g is continuous, then hs.extend f = g.

Русский

Пусть hs плотная подмножество. Если для всех x ∈ α: g(i x) = f x и g непрерывна, то hs.extend f = g.

LaTeX

$$$\\\\forall x, \\\\; g(i x) = f x \\\\Rightarrow \\\\; \\mathrm{extend} f = g$ (при непрерывности g)$$

Lean4

theorem extend_unique [T2Space β] {g : α → β} (hs : Dense s) (hf : ∀ x : s, g x = f x) (hg : Continuous g) :
    hs.extend f = g :=
  hs.isDenseInducing_val.extend_unique hf hg

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