extensionEmbedding_of_comp_coe — Mathlib

English

There is an isometry extension: extensionEmbedding_of_comp is an isometry.

Русский

Существует изометрическое продолжение: extensionEmbedding_of_comp является изометрией.

LaTeX

$$$$Isometry( extensionEmbedding\\_of\\_comp(h) ).$$$$

Lean4

theorem extensionEmbedding_of_comp_coe (h : ∀ x, ‖f x‖ = v x) (x : K) : extensionEmbedding_of_comp h x = f x := by
  rw [← UniformSpace.Completion.extensionHom_coe f (WithAbs.isUniformInducing_of_comp h).uniformContinuous.continuous]

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