α : Type u
β : Type v
X : Type ?u.42927
ι : Type ?u.42930
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : Set.Nonempty (closedBall y ε₂ ∩ ball x ε₁)
⊢ dist x y < ε₁ + ε₂
α : Type u
β : Type v
X : Type ?u.42927
ι : Type ?u.42930
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : Set.Nonempty (ball x ε₁ ∩ closedBall y ε₂)
⊢ dist x y < ε₁ + ε₂
rw [inter_comm] at h
α : Type u
β : Type v
X : Type ?u.42927
ι : Type ?u.42930
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : Set.Nonempty (closedBall y ε₂ ∩ ball x ε₁)
⊢ dist y x < ε₂ + ε₁
α : Type u
β : Type v
X : Type ?u.42927
ι : Type ?u.42930
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : Set.Nonempty (closedBall y ε₂ ∩ ball x ε₁)
⊢ dist x y < ε₁ + ε₂
rw [add_comm, dist_comm]
no goals
α : Type u
β : Type v
X : Type ?u.42927
ι : Type ?u.42930
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : Set.Nonempty (closedBall y ε₂ ∩ ball x ε₁)
⊢ dist y x < ε₂ + ε₁
exact dist_lt_add_of_nonempty_closedBall_inter_ball h