no goals
α : Type u
β : Type v
γ : Type ?u.211843
δ : Type ?u.211846
ε : Type ?u.211849
ζ : Type ?u.211852
ι : Type ?u.211855
π✝ : ι → Type ?u.211860
κ : Type ?u.211863
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
n : ℕ
π : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : β → π i
l : Filter β
x : π i
hf : Tendsto f l (𝓝 x)
g : β → (j : Fin n) → π (↑(Fin.succAbove i) j)
y : (j : Fin n) → π (↑(Fin.succAbove i) j)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i_1 => Fin.insertNth i (f i_1) (g i_1) i) l (𝓝 (Fin.insertNth i x y i))
simpa
no goals
α : Type u
β : Type v
γ : Type ?u.211843
δ : Type ?u.211846
ε : Type ?u.211849
ζ : Type ?u.211852
ι : Type ?u.211855
π✝ : ι → Type ?u.211860
κ : Type ?u.211863
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π✝ i)
f✝ : α → (i : ι) → π✝ i
n : ℕ
π : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
i : Fin (n + 1)
f : β → π i
l : Filter β
x : π i
hf : Tendsto f l (𝓝 x)
g : β → (j : Fin n) → π (↑(Fin.succAbove i) j)
y : (j : Fin n) → π (↑(Fin.succAbove i) j)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (j : Fin n),
    Tendsto (fun i_1 => Fin.insertNth i (f i_1) (g i_1) (↑(Fin.succAbove i) j)) l
      (𝓝 (Fin.insertNth i x y (↑(Fin.succAbove i) j)))
simpa using tendsto_pi_nhds.1 hg