no goals
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.fst) (Completion.extension f x.snd)
continuity
no goals
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => ↑K * dist x.fst x.snd
continuity
no goals
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f (↑α a)) (Completion.extension f (↑α b)) ≤ ↑K * dist (↑α a) (↑α b)
simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul