α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
⊢ HasBasis (𝓝 x ×ˢ 𝓝 y) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
⊢ HasBasis (𝓝 (x, y)) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
rw [nhds_prod_eq]
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : Set (α × α)},
    i ∈ 𝓤 α ∧ SymmetricRel i →
      j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
⊢ HasBasis (𝓝 x ×ˢ 𝓝 y) (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s ×ˢ ball y s
apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
U V : Set (α × α)
U_in : U ∈ 𝓤 α
U_symm : SymmetricRel U
V_in : V ∈ 𝓤 α
V_symm : SymmetricRel V
⊢ ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
⊢ ∀ {i j : Set (α × α)},
    i ∈ 𝓤 α ∧ SymmetricRel i →
      j ∈ 𝓤 α ∧ SymmetricRel j → ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩
no goals
case intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.69859
inst✝ : UniformSpace α
x y : α
U V : Set (α × α)
U_in : U ∈ 𝓤 α
U_symm : SymmetricRel U
V_in : V ∈ 𝓤 α
V_symm : SymmetricRel V
⊢ ∃ k, (k ∈ 𝓤 α ∧ SymmetricRel k) ∧ ball x k ⊆ ball x U ∧ ball y k ⊆ ball y V
exact
  ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, U_symm.inter V_symm⟩, ball_inter_left x U V,
    ball_inter_right y U V⟩