completion_extension — Mathlib

English

If f is an isometry, its extension to the completion is also an isometry.

Русский

Если f — изометрия, её продолжение до завершения также является изометрией.

LaTeX

$$$\text{Isometry } f \Rightarrow \text{Isometry } (\mathrm{Completion}.extension f)$$$

Lean4

theorem completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β} {K : ℝ≥0} (h : LipschitzWith K f) :
    LipschitzWith K (Completion.extension f) :=
  LipschitzWith.of_dist_le_mul fun x y =>
    induction_on₂ x y (isClosed_le (by fun_prop) (by fun_prop)) <| by
      simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

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