α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α
intro V V_in
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)

case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)
apply mem_of_superset this
case intro.intro.intro.mk.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).fst ∈ ball x w
v_in : (u, v).snd ∈ ball x w
⊢ (u, v) ∈ V
case intro.intro.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V
rintro ⟨u, v⟩ ⟨u_in, v_in⟩
no goals
case intro.intro.intro.mk.intro
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).fst ∈ ball x w
v_in : (u, v).snd ∈ ball x w
⊢ (u, v) ∈ V
exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
rw [nhds_prod_eq]
no goals
case this
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.84873
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)