isometry_extensionEmbedding_of_comp

English

If f is an embedding of the WithAbs v into a normed field L, its extension embedding is an isometry.

Русский

Если f является вложением WithAbs v в нормированное поле L, то его расширенное вложение — это изометрия.

LaTeX

$$$$Isometry( extensionEmbedding_of_comp(h) ).$$$$

Lean4

/-- If the absolute value of a normed field factors through an embedding into another normed field,
then the extended embedding `v.Completion →+* L` is an isometry. -/
theorem isometry_extensionEmbedding_of_comp (h : ∀ x, ‖f x‖ = v x) : Isometry (extensionEmbedding_of_comp h) :=
  Isometry.of_dist_eq <| extensionEmbedding_dist_eq_of_comp h

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