X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Tendsto (fun i => restrict K (∑ b in i, F b)) atTop (𝓝 f)
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
⊢ Summable F
refine' (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => _
case intro
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Tendsto (fun i => restrict K (∑ b in i, F b)) atTop (𝓝 f)
lift K to Compacts X using hK
case intro
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
case intro
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
have A : ∀ s : Finset ι, restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict K (F i) := by
  intro s
  ext1 x
  simp
no goals
case intro
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
⊢ ∃ f, Tendsto (fun i => restrict (↑K) (∑ b in i, F b)) atTop (𝓝 f)
simpa only [HasSum, A] using summable_of_summable_norm (hF K)
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∀ (s : Finset ι), restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
intro s
case h
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ↑(restrict (↑K) (∑ i in s, F i)) x = ↑(∑ i in s, restrict (↑K) (F i)) x
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i in s, F i) = ∑ i in s, restrict (↑K) (F i)
ext1 x
no goals
case h
X : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_1
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ↑(restrict (↑K) (∑ i in s, F i)) x = ↑(∑ i in s, restrict (↑K) (F i)) x
simp