ι : Type ?u.1994
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
ι : Type ?u.1994
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
inst✝ : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y
rw [Subsingleton.elim x y]
no goals
ι : Type ?u.1994
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
simp