ι : Type ?u.45267
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s : Set α
hf : Isometry f
⊢ EMetric.diam (f '' univ) = EMetric.diam univ
ι : Type ?u.45267
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s : Set α
hf : Isometry f
⊢ EMetric.diam (range f) = EMetric.diam univ
rw [← image_univ]
no goals
ι : Type ?u.45267
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s : Set α
hf : Isometry f
⊢ EMetric.diam (f '' univ) = EMetric.diam univ
exact hf.ediam_image univ