extension_unique — Mathlib

English

The extension is unique: if g on Completion G agrees with f on G, then f.extension = g.

Русский

Расширение единственно: если g на Completion(G) совпадает с f на G, то f.extension = g.

LaTeX

$$$ f.extension = g \quad \text{whenever } \forall v, f(v) = g(v).$$$

Lean4

theorem extension_unique (f : NormedAddGroupHom G H) {g : NormedAddGroupHom (Completion G) H} (hg : ∀ v, f v = g v) :
    f.extension = g := by
  ext v
  rw [NormedAddGroupHom.extension_coe_to_fun,
    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]

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