ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ i in s, f i
refine' cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => _
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i in t, f i‖ < ε
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
⊢ ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
refine' ⟨s ∪ h.toFinset, fun t ht => _⟩
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ (i : ι), i ∈ t → ‖f i‖ ≤ g i
⊢ ‖∑ i in t, f i‖ < ε
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i in t, f i‖ < ε
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
  intro i hi
  simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
    Classical.not_not] at ht
  exact (ht hi).2
no goals
case intro
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ (i : ι), i ∈ t → ‖f i‖ ≤ g i
⊢ ‖∑ i in t, f i‖ < ε
calc
  ‖∑ i in t, f i‖ ≤ ∑ i in t, g i := norm_sum_le_of_le _ this
  _ ≤ ‖∑ i in t, g i‖ := (le_abs_self _)
  _ < ε := hs _ (ht.mono_right le_sup_left)
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ∀ (i : ι), i ∈ t → ‖f i‖ ≤ g i
intro i hi
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → ¬a ∈ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i
simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
  Classical.not_not] at ht
no goals
ι : Type u_1
α : Type ?u.3377
E : Type u_2
F : Type ?u.3383
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → ¬a ∈ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i
exact (ht hi).2