𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ Continuous ↑(Basis.equivFun ξ)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
⊢ Continuous ↑(Basis.equivFun ξ)
letI : UniformSpace E := TopologicalAddGroup.toUniformSpace E
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
⊢ Continuous ↑(Basis.equivFun ξ)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ Continuous ↑(Basis.equivFun ξ)
letI : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
⊢ Continuous ↑(Basis.equivFun ξ)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
⊢ Continuous ↑(Basis.equivFun ξ)
letI : SeparatedSpace E := separated_iff_t2.mpr ht2
case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.zero
⊢ Continuous ↑(Basis.equivFun ξ)

case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
⊢ Continuous ↑(Basis.equivFun ξ)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜 E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : TopologicalAddGroup E
inst✝¹² : ContinuousSMul 𝕜 E
F : Type w
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : TopologicalSpace F
inst✝⁸ : TopologicalAddGroup F
inst✝⁷ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
⊢ Continuous ↑(Basis.equivFun ξ)
induction' hn : Fintype.card ι with n IH generalizing ι E
case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : IsEmpty ι
⊢ Continuous ↑(Basis.equivFun ξ)
case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.zero
⊢ Continuous ↑(Basis.equivFun ξ)
rw [Fintype.card_eq_zero_iff] at hn
no goals
case zero
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : IsEmpty ι
⊢ Continuous ↑(Basis.equivFun ξ)
exact continuous_of_const fun x y => funext hn.elim
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
⊢ Continuous ↑(Basis.equivFun ξ)
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁴ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝³ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
⊢ Continuous ↑(Basis.equivFun ξ)
haveI : FiniteDimensional 𝕜 E := of_fintype_basis ξ
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
⊢ Continuous ↑(Basis.equivFun ξ)
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
⊢ Continuous ↑(Basis.equivFun ξ)
have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by
  intro s s_dim
  letI : UniformAddGroup s := s.toAddSubgroup.uniformAddGroup
  let b := Basis.ofVectorSpace 𝕜 s
  have U : UniformEmbedding b.equivFun.symm.toEquiv := by
    have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
      rw [← s_dim]
      exact (finrank_eq_card_basis b).symm
    have : Continuous b.equivFun := IH b this
    exact
      b.equivFun.symm.uniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
  have : IsComplete (s : Set E) :=
    completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 (by infer_instance))
  exact this.isClosed
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
⊢ ∀ (i : ι), Continuous fun a => ↑(Basis.equivFun ξ) a i
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
⊢ Continuous ↑(Basis.equivFun ξ)
rw [continuous_pi_iff]
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
i : ι
⊢ Continuous fun a => ↑(Basis.equivFun ξ) a i
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
⊢ ∀ (i : ι), Continuous fun a => ↑(Basis.equivFun ξ) a i
intro i
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
i : ι
⊢ Continuous ↑(Basis.coord ξ i)
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
i : ι
⊢ Continuous fun a => ↑(Basis.equivFun ξ) a i
change Continuous (ξ.coord i)
no goals
case succ
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
H₂ : ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
i : ι
⊢ Continuous ↑(Basis.coord ξ i)
exact H₂ (ξ.coord i)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
⊢ IsClosed ↑s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
⊢ ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
intro s s_dim
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
⊢ IsClosed ↑s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
⊢ IsClosed ↑s
letI : UniformAddGroup s := s.toAddSubgroup.uniformAddGroup
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ IsClosed ↑s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
⊢ IsClosed ↑s
let b := Basis.ofVectorSpace 𝕜 s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
U : UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
⊢ IsClosed ↑s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ IsClosed ↑s
have U : UniformEmbedding b.equivFun.symm.toEquiv := by
  have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
    rw [← s_dim]
    exact (finrank_eq_card_basis b).symm
  have : Continuous b.equivFun := IH b this
  exact
    b.equivFun.symm.uniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
U : UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
this : IsComplete ↑s
⊢ IsClosed ↑s
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
U : UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
⊢ IsClosed ↑s
have : IsComplete (s : Set E) :=
  completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 (by infer_instance))
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
U : UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
this : IsComplete ↑s
⊢ IsClosed ↑s
exact this.isClosed
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
this : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = n
⊢ UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
  rw [← s_dim]
  exact (finrank_eq_card_basis b).symm
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁸ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁷ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁶ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁵ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝⁴ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝² : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝¹ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
this✝ : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = n
this : Continuous ↑(Basis.equivFun b)
⊢ UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
this : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = n
⊢ UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
have : Continuous b.equivFun := IH b this
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁸ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁷ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁶ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁵ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝⁴ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝² : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this✝¹ : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
this✝ : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = n
this : Continuous ↑(Basis.equivFun b)
⊢ UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
exact
  b.equivFun.symm.uniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = finrank 𝕜 { x // x ∈ s }
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = n
rw [← s_dim]
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
⊢ Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) = finrank 𝕜 { x // x ∈ s }
exact (finrank_eq_card_basis b).symm
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 { x // x ∈ s } = n
this : UniformAddGroup { x // x ∈ s } := AddSubgroup.uniformAddGroup (Submodule.toAddSubgroup s)
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s })) 𝕜 { x // x ∈ s } := Basis.ofVectorSpace 𝕜 { x // x ∈ s }
U : UniformEmbedding ↑(LinearEquiv.toEquiv (LinearEquiv.symm (Basis.equivFun b)))
⊢ CompleteSpace (↑(Basis.ofVectorSpaceIndex 𝕜 { x // x ∈ s }) → 𝕜)
infer_instance
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
⊢ Continuous ↑f
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
⊢ ∀ (f : E →ₗ[𝕜] 𝕜), Continuous ↑f
intro f
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
⊢ Continuous ↑f

case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
⊢ Continuous ↑f
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
⊢ Continuous ↑f
by_cases H : finrank 𝕜 (LinearMap.range f) = 0
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous ↑f
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
⊢ Continuous ↑f
rw [finrank_eq_zero, LinearMap.range_eq_bot] at H
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous ↑0
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous ↑f
rw [H]
no goals
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous ↑0
exact continuous_zero
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
this : finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
⊢ Continuous ↑f
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
⊢ Continuous ↑f
have : finrank 𝕜 (LinearMap.ker f) = n := by
  have Z := f.finrank_range_add_finrank_ker
  rw [finrank_eq_card_basis ξ, hn] at Z
  have : finrank 𝕜 (LinearMap.range f) = 1 :=
    le_antisymm (finrank_self 𝕜 ▸ f.range.finrank_le) (zero_lt_iff.mpr H)
  rw [this, add_comm, Nat.add_one] at Z
  exact Nat.succ.inj Z
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
this✝ : finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
this : IsClosed ↑(LinearMap.ker f)
⊢ Continuous ↑f
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
this : finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
⊢ Continuous ↑f
have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
no goals
case neg
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁷ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁶ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁵ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝⁴ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝³ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝² : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝¹ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
this✝ : finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
this : IsClosed ↑(LinearMap.ker f)
⊢ Continuous ↑f
exact LinearMap.continuous_of_isClosed_ker f this
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = finrank 𝕜 E
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
have Z := f.finrank_range_add_finrank_ker
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = Nat.succ n
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = finrank 𝕜 E
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
rw [finrank_eq_card_basis ξ, hn] at Z
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = Nat.succ n
this : finrank 𝕜 { x // x ∈ LinearMap.range f } = 1
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁵ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁴ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝³ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝² : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝¹ : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = Nat.succ n
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
have : finrank 𝕜 (LinearMap.range f) = 1 :=
  le_antisymm (finrank_self 𝕜 ▸ f.range.finrank_le) (zero_lt_iff.mpr H)
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : Nat.succ (finrank 𝕜 { x // x ∈ LinearMap.ker f }) = Nat.succ n
this : finrank 𝕜 { x // x ∈ LinearMap.range f } = 1
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : finrank 𝕜 { x // x ∈ LinearMap.range f } + finrank 𝕜 { x // x ∈ LinearMap.ker f } = Nat.succ n
this : finrank 𝕜 { x // x ∈ LinearMap.range f } = 1
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
rw [this, add_comm, Nat.add_one] at Z
no goals
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E✝ : Type v
inst✝²² : AddCommGroup E✝
inst✝²¹ : Module 𝕜 E✝
inst✝²⁰ : TopologicalSpace E✝
inst✝¹⁹ : TopologicalAddGroup E✝
inst✝¹⁸ : ContinuousSMul 𝕜 E✝
F : Type w
inst✝¹⁷ : AddCommGroup F
inst✝¹⁶ : Module 𝕜 F
inst✝¹⁵ : TopologicalSpace F
inst✝¹⁴ : TopologicalAddGroup F
inst✝¹³ : ContinuousSMul 𝕜 F
F' : Type x
inst✝¹² : AddCommGroup F'
inst✝¹¹ : Module 𝕜 F'
inst✝¹⁰ : TopologicalSpace F'
inst✝⁹ : TopologicalAddGroup F'
inst✝⁸ : ContinuousSMul 𝕜 F'
inst✝⁷ : CompleteSpace 𝕜
ht2✝ : T2Space E✝
ι✝ : Type v
inst✝⁶ : Fintype ι✝
ξ✝ : Basis ι✝ 𝕜 E✝
this✝⁶ : UniformSpace E✝ := TopologicalAddGroup.toUniformSpace E✝
this✝⁵ : UniformAddGroup E✝ := comm_topologicalAddGroup_is_uniform
this✝⁴ : SeparatedSpace E✝ := Iff.mpr separated_iff_t2 ht2✝
x✝ : ℕ
hn✝ : Fintype.card ι✝ = x✝
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [ht2 : T2Space E] {ι : Type v} [inst_5 : Fintype ι]
    (ξ : Basis ι 𝕜 E),
    let this := TopologicalAddGroup.toUniformSpace E;
    let this_1 := (_ : UniformAddGroup E);
    let this := (_ : SeparatedSpace E);
    Fintype.card ι = n → Continuous ↑(Basis.equivFun ξ)
E : Type v
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
ht2 : T2Space E
ι : Type v
inst✝ : Fintype ι
ξ : Basis ι 𝕜 E
this✝³ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝² : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
this✝¹ : SeparatedSpace E := Iff.mpr separated_iff_t2 ht2
hn : Fintype.card ι = Nat.succ n
this✝ : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 { x // x ∈ s } = n → IsClosed ↑s
f : E →ₗ[𝕜] 𝕜
H : ¬finrank 𝕜 { x // x ∈ LinearMap.range f } = 0
Z : Nat.succ (finrank 𝕜 { x // x ∈ LinearMap.ker f }) = Nat.succ n
this : finrank 𝕜 { x // x ∈ LinearMap.range f } = 1
⊢ finrank 𝕜 { x // x ∈ LinearMap.ker f } = n
exact Nat.succ.inj Z