isClosedEmbedding_extensionEmbedding_of_comp

English

The extension embedding is a closed embedding; in particular, the image is closed and the map is an embedding.

Русский

Расширенное вложение является замкнутым вложением; в частности, образ замкнут и отображение — вложение.

LaTeX

$$$$IsClosedEmbedding( 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 a closed embedding. -/
theorem isClosedEmbedding_extensionEmbedding_of_comp (h : ∀ x, ‖f x‖ = v x) :
    IsClosedEmbedding (extensionEmbedding_of_comp h) :=
  (isometry_extensionEmbedding_of_comp h).isClosedEmbedding

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