case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
cases nonempty_fintype ι
case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
simp only [Fintype.linearIndependent_iff'] at hf⊢
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
  tendsto_finset_sum _ fun i _ =>
    Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
refine' (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => _
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ∑ i : ι, ‖g i - f i‖₊ < K⁻¹

case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
⊢ LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
replace hg : (∑ i, ‖g i - f i‖₊) < K⁻¹
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
⊢ Function.Injective ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i))
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
⊢ LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) = ⊥
rw [LinearMap.ker_eq_bot]
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ dist
      ((↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) -
          ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)))
        v)
      ((↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) -
          ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)))
        u) ≤
    ↑(∑ i : ι, ‖g i - f i‖₊) * dist v u
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
⊢ Function.Injective ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i))
refine' (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => _) hg).injective
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ ‖∑ x : ι, (v x - u x) • (g x - f x)‖ ≤ ∑ x : ι, ‖g x - f x‖ * ‖v - u‖
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ dist
      ((↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) -
          ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)))
        v)
      ((↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (g i)) -
          ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)))
        u) ≤
    ↑(∑ i : ι, ‖g i - f i‖₊) * dist v u
simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,
  LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←
  Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ ‖∑ x : ι, (v x - u x) • (g x - f x)‖ ≤ ∑ x : ι, ‖g x - f x‖ * ‖v - u‖
refine' norm_sum_le_of_le _ fun i _ => _
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
rw [norm_smul, mul_comm]
case intro.intro.intro.h
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ ≤ ‖v - u‖
case intro.intro.intro
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
gcongr
no goals
case intro.intro.intro.h
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ ≤ ‖v - u‖
exact norm_le_pi_norm (v - u) i
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ↑(∑ i : ι, ‖g i - f i‖₊) < ↑K⁻¹
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
rw [← NNReal.coe_lt_coe]
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ∑ x : ι, ‖g x - f x‖ < (↑K)⁻¹
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ↑(∑ i : ι, ‖g i - f i‖₊) < ↑K⁻¹
push_cast
no goals
case hg
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker (↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ↑(↑(LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.smulRight LinearMap.id (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ∑ x : ι, ‖g x - f x‖ < (↑K)⁻¹
exact hg