α : Type u
β : Type v
X : Type ?u.155993
ι : Type ?u.155996
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : Set.Nonempty (ball x ε)
⊢ ∃ y, y ∈ s ∧ dist x y < ε
α : Type u
β : Type v
X : Type ?u.155993
ι : Type ?u.155996
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ y, y ∈ s ∧ dist x y < ε
have : (ball x ε).Nonempty := by simp [hε]
no goals
α : Type u
β : Type v
X : Type ?u.155993
ι : Type ?u.155996
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : Set.Nonempty (ball x ε)
⊢ ∃ y, y ∈ s ∧ dist x y < ε
simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this
no goals
α : Type u
β : Type v
X : Type ?u.155993
ι : Type ?u.155996
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s✝ s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ Set.Nonempty (ball x ε)
simp [hε]