English
For h, and x in K, the value of the extended embedding on the coerced element equals f x; i.e., extensionEmbedding_of_comp h x = f x when appropriately identified.
Русский
Для h и x ∈ K значение расширенного вложения на соответствующий элемент равно f x; т. е. extensionEmbedding_of_comp(h) x = f x при надлежащем сведении.
LaTeX
$$$$extensionEmbedding_of_comp(h)(x)=f(x)\\quad (x\\in K).$$$$
Lean4
/-- If the absolute value of a normed field factors through an embedding into another normed field,
then the extended embedding `v.Completion →+* L` preserves distances. -/
theorem extensionEmbedding_dist_eq_of_comp (h : ∀ x, ‖f x‖ = v x) (x y : v.Completion) :
dist (extensionEmbedding_of_comp h x) (extensionEmbedding_of_comp h y) = dist x y :=
by
refine UniformSpace.Completion.induction_on₂ x y ?_ (fun x y => ?_)
· refine isClosed_eq ?_ continuous_dist
exact continuous_iff_continuous_dist.1 UniformSpace.Completion.continuous_extension
· simp only [extensionEmbedding_of_comp_coe]
exact UniformSpace.Completion.dist_eq x y ▸ (WithAbs.isometry_of_comp h).dist_eq _ _
