ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b in t, f b ∈ ball 0 i) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε

ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b in t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ (CauchySeq fun s => ∑ i in s, f i) ↔ ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
rw [cauchySeq_finset_iff_vanishing, nhds_basis_ball.forall_iff]
no goals
ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ (∀ (i : ℝ), 0 < i → ∃ s, ∀ (t : Finset ι), Disjoint t s → ∑ b in t, f b ∈ ball 0 i) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i in t, f i‖ < ε
simp only [ball_zero_eq, Set.mem_setOf_eq]
case intro
ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b in t, f b ∈ s
⊢ ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
⊢ ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ s_1, ∀ (t : Finset ι), Disjoint t s_1 → ∑ b in t, f b ∈ s) →
        ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
rintro s t hst ⟨s', hs'⟩
no goals
case intro
ι : Type u_2
α : Type ?u.23
E : Type u_1
F : Type ?u.29
inst✝¹ : SeminormedAddCommGroup E
inst✝ : SeminormedAddCommGroup F
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b in t, f b ∈ s
⊢ ∃ s, ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b in t_1, f b ∈ t
exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩