α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.92331
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i j, y ∈ ball i U
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.92331
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
⊢ (⋃ (x : α) (_ : x ∈ s), ball x U) = univ
refine' iUnion₂_eq_univ_iff.2 fun y => _
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.92331
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i j, y ∈ ball i U
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.92331
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i j, y ∈ ball i U
rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩
no goals
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.92331
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i j, y ∈ ball i U
exact ⟨x, hxs, hxy⟩