no goals
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry 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 : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist x.fst x.snd
continuity
no goals
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
x✝¹ x✝ : α
⊢ dist (Completion.extension f (↑α x✝¹)) (Completion.extension f (↑α x✝)) = dist (↑α x✝¹) (↑α x✝)
simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]