α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist b✝ a✝ < ε
⊢ dist (-a✝) (-b✝) < ε
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist a✝ b✝ < ε
⊢ dist (-a✝) (-b✝) < ε
rw [dist_comm] at h
no goals
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist b✝ a✝ < ε
⊢ dist (-a✝) (-b✝) < ε
simpa only [Real.dist_eq, neg_sub_neg] using h