case mk
α : Type u
β : Type v
γ : Type ?u.527144
δ : Type ?u.527147
ε : Type ?u.527150
ζ : Type ?u.527153
ι : Type u_1
κ : Type ?u.527159
σ : ι → Type u_2
τ : κ → Type ?u.527169
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 { fst := fst✝, snd := snd✝ } = Filter.map (mk { fst := fst✝, snd := snd✝ }.fst) (𝓝 { fst := fst✝, snd := snd✝ }.snd)
α : Type u
β : Type v
γ : Type ?u.527144
δ : Type ?u.527147
ε : Type ?u.527150
ζ : Type ?u.527153
ι : Type u_1
κ : Type ?u.527159
σ : ι → Type u_2
τ : κ → Type ?u.527169
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk x.fst) (𝓝 x.snd)
cases x
no goals
case mk
α : Type u
β : Type v
γ : Type ?u.527144
δ : Type ?u.527147
ε : Type ?u.527150
ζ : Type ?u.527153
ι : Type u_1
κ : Type ?u.527159
σ : ι → Type u_2
τ : κ → Type ?u.527169
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 { fst := fst✝, snd := snd✝ } = Filter.map (mk { fst := fst✝, snd := snd✝ }.fst) (𝓝 { fst := fst✝, snd := snd✝ }.snd)
apply Sigma.nhds_mk