extensionEmbedding_of_comp — Mathlib

English

The extensionEmbedding_of_comp is the canonical embedding of v.Completion into L when h holds; it extends f from WithAbs v to L.

Русский

extensionEmbedding_of_comp является каноническим вложением v.Completion в L при условии h; оно продолжает f из WithAbs v в L.

LaTeX

$$$$extensionEmbedding\\_of\\_comp(h) : v.Completion \\to+* L.$$$$

Lean4

/-- If the absolute value of a normed field factors through an embedding into another normed field
`L`, then we can extend that embedding to an embedding on the completion `v.Completion →+* L`. -/
abbrev extensionEmbedding_of_comp (h : ∀ x, ‖f x‖ = v x) : v.Completion →+* L :=
  UniformSpace.Completion.extensionHom _ (WithAbs.isUniformInducing_of_comp h).uniformContinuous.continuous

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