completion_map — Mathlib

English

If f is Lipschitz with constant K, then the induced map on the completion is Lipschitz with the same constant.

Русский

Если f липшицево с константой K, то отображение на завершение также липшицево с той же константой.

LaTeX

$$$\text{LipschitzWith } K f \Rightarrow \text{LipschitzWith } K (\mathrm{Completion}.map f)$$$

Lean4

theorem completion_map [PseudoMetricSpace β] {f : α → β} {K : ℝ≥0} (h : LipschitzWith K f) :
    LipschitzWith K (Completion.map f) :=
  one_mul K ▸ (coe_isometry.lipschitz.comp h).completion_extension

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