[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ t = UniformSpace.toTopologicalSpace
[PROOFSTEP]
refine' TopologicalAddGroup.ext h₁ inferInstance (le_antisymm _ _)
[GOAL]
case refine'_1
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ nhds 0 ≤ nhds 0
[PROOFSTEP]
rw [Metric.nhds_basis_closedBall.ge_iff]
  -- Let `ε > 0`. Since `𝕜` is nontrivially normed, we have `0 < ‖ξ₀‖ < ε` for some `ξ₀ : 𝕜`.
[GOAL]
case refine'_1
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ ∀ (i' : ℝ), 0 < i' → Metric.closedBall 0 i' ∈ nhds 0
[PROOFSTEP]
intro ε hε
[GOAL]
case refine'_1
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
⊢ Metric.closedBall 0 ε ∈ nhds 0
[PROOFSTEP]
rcases NormedField.exists_norm_lt 𝕜 hε with
  ⟨ξ₀, hξ₀, hξ₀ε⟩
    -- Since `ξ₀ ≠ 0` and `𝓣` is T2, we know that `{ξ₀}ᶜ` is a `𝓣`-neighborhood of 0.
        -- Porting note: added `mem_compl_singleton_iff.mpr`
[GOAL]
case refine'_1.intro.intro
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
⊢ Metric.closedBall 0 ε ∈ nhds 0
[PROOFSTEP]
have : { ξ₀ }ᶜ ∈ @nhds 𝕜 t 0 :=
  IsOpen.mem_nhds isOpen_compl_singleton <| mem_compl_singleton_iff.mpr <| Ne.symm <| norm_ne_zero_iff.mp hξ₀.ne.symm
[GOAL]
case refine'_1.intro.intro
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this : {ξ₀}ᶜ ∈ nhds 0
⊢ Metric.closedBall 0 ε ∈ nhds 0
[PROOFSTEP]
have : balancedCore 𝕜 { ξ₀ }ᶜ ∈ @nhds 𝕜 t 0 := balancedCore_mem_nhds_zero this
[GOAL]
case refine'_1.intro.intro
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
⊢ Metric.closedBall 0 ε ∈ nhds 0
[PROOFSTEP]
refine'
  mem_of_superset this fun ξ hξ =>
    _
      -- Let `ξ ∈ 𝓑`. We want to show `‖ξ‖ < ε`. If `ξ = 0`, this is trivial.
[GOAL]
case refine'_1.intro.intro
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ ξ ∈ Metric.closedBall 0 ε
[PROOFSTEP]
by_cases hξ0 : ξ = 0
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ξ = 0
⊢ ξ ∈ Metric.closedBall 0 ε
[PROOFSTEP]
rw [hξ0]
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ξ = 0
⊢ 0 ∈ Metric.closedBall 0 ε
[PROOFSTEP]
exact Metric.mem_closedBall_self hε.le
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
⊢ ξ ∈ Metric.closedBall 0 ε
[PROOFSTEP]
rw [mem_closedBall_zero_iff]
  -- Now suppose `ξ ≠ 0`. By contradiction, let's assume `ε < ‖ξ‖`, and show that
        -- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction.
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
⊢ ‖ξ‖ ≤ ε
[PROOFSTEP]
by_contra' h
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ False
[PROOFSTEP]
suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 { ξ₀ }ᶜ
  by
  rw [smul_eq_mul 𝕜, mul_assoc, inv_mul_cancel hξ0, mul_one] at this
  exact
    not_mem_compl_iff.mpr (mem_singleton ξ₀)
      ((balancedCore_subset _) this)
        -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,
              -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝¹ : {ξ₀}ᶜ ∈ nhds 0
this✝ : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False
[PROOFSTEP]
rw [smul_eq_mul 𝕜, mul_assoc, inv_mul_cancel hξ0, mul_one] at this
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝¹ : {ξ₀}ᶜ ∈ nhds 0
this✝ : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
this : ξ₀ ∈ balancedCore 𝕜 {ξ₀}ᶜ
⊢ False
[PROOFSTEP]
exact
  not_mem_compl_iff.mpr (mem_singleton ξ₀)
    ((balancedCore_subset _) this)
      -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,
            -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
[PROOFSTEP]
refine' (balancedCore_balanced _).smul_mem _ hξ
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ ‖ξ₀ * ξ⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_mul, norm_inv, mul_inv_le_iff (norm_pos_iff.mpr hξ0), mul_one]
[GOAL]
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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
ε : ℝ
hε : 0 < ε
ξ₀ : 𝕜
hξ₀ : 0 < ‖ξ₀‖
hξ₀ε : ‖ξ₀‖ < ε
this✝ : {ξ₀}ᶜ ∈ nhds 0
this : balancedCore 𝕜 {ξ₀}ᶜ ∈ nhds 0
ξ : 𝕜
hξ : ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ
hξ0 : ¬ξ = 0
h : ε < ‖ξ‖
⊢ ‖ξ₀‖ ≤ ‖ξ‖
[PROOFSTEP]
exact (hξ₀ε.trans h).le
[GOAL]
case refine'_2
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ nhds 0 ≤ nhds 0
[PROOFSTEP]
calc
  @nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0 = map id (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) :=
    map_id.symm
  _ = map (fun x => id x • (1 : 𝕜)) (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) := by
    conv_rhs =>
      congr
      ext
      rw [smul_eq_mul, mul_one]
  _ ≤ @nhds 𝕜 t ((0 : 𝕜) • (1 : 𝕜)) :=
    (@Tendsto.smul_const _ _ _ hnorm.toUniformSpace.toTopologicalSpace t _ _ _ _ _ tendsto_id (1 : 𝕜))
  _ = @nhds 𝕜 t 0 := by rw [zero_smul]
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ map id (nhds 0) = map (fun x => id x • 1) (nhds 0)
[PROOFSTEP]
conv_rhs =>
  congr
  ext
  rw [smul_eq_mul, mul_one]
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| map (fun x => id x • 1) (nhds 0)
[PROOFSTEP]
  congr
  ext
  rw [smul_eq_mul, mul_one]
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| map (fun x => id x • 1) (nhds 0)
[PROOFSTEP]
  congr
  ext
  rw [smul_eq_mul, mul_one]
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| map (fun x => id x • 1) (nhds 0)
[PROOFSTEP]
congr
[GOAL]
case m
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| fun x => id x • 1
case 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| nhds 0
[PROOFSTEP]
ext
[GOAL]
case m.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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
x✝ : 𝕜
| id x✝ • 1
case 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
| nhds 0
[PROOFSTEP]
rw [smul_eq_mul, mul_one]
[GOAL]
𝕜 : 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'
t : TopologicalSpace 𝕜
h₁ : TopologicalAddGroup 𝕜
h₂ : ContinuousSMul 𝕜 𝕜
h₃ : T2Space 𝕜
⊢ nhds (0 • 1) = nhds 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
⊢ Continuous ↑l
[PROOFSTEP]
by_cases H : finrank 𝕜 (LinearMap.range l) = 0
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l
[PROOFSTEP]
rw [finrank_eq_zero, LinearMap.range_eq_bot] at H
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑l
[PROOFSTEP]
rw [H]
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : l = 0
⊢ Continuous ↑0
[PROOFSTEP]
exact continuous_zero
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
⊢ Continuous ↑l
[PROOFSTEP]
have : finrank 𝕜 (LinearMap.range l) = 1 := le_antisymm (finrank_self 𝕜 ▸ l.range.finrank_le) (zero_lt_iff.mpr H)
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ Continuous ↑l
[PROOFSTEP]
have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) :=
  by
  rw [← LinearMap.ker_eq_bot]
  exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
[PROOFSTEP]
rw [← LinearMap.ker_eq_bot]
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
⊢ ker (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) = ⊥
[PROOFSTEP]
exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
[PROOFSTEP]
have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) :=
  by
  rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
  exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
[PROOFSTEP]
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ range l = ⊤
[PROOFSTEP]
exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
⊢ Continuous ↑l
[PROOFSTEP]
let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 := LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
⊢ Continuous ↑l
[PROOFSTEP]
have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext;
  rfl
    -- Since the quotient map `E →ₗ[𝕜] (E ⧸ l.ker)` is continuous, the continuity of `l` will follow
        -- form the continuity of `φ`.
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
⊢ ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
[PROOFSTEP]
ext
[GOAL]
case 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
x✝ : E
⊢ ↑l x✝ = (↑φ ∘ ↑(Submodule.mkQ (ker l))) x✝
[PROOFSTEP]
rfl
  -- Since the quotient map `E →ₗ[𝕜] (E ⧸ l.ker)` is continuous, the continuity of `l` will follow
      -- form the continuity of `φ`.
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑l
[PROOFSTEP]
suffices Continuous φ.toEquiv by
  rw [hlφ]
  exact this.comp continuous_quot_mk
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : Continuous ↑(LinearEquiv.toEquiv φ)
⊢ Continuous ↑l
[PROOFSTEP]
rw [hlφ]
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : Continuous ↑(LinearEquiv.toEquiv φ)
⊢ Continuous (↑φ ∘ ↑(Submodule.mkQ (ker l)))
[PROOFSTEP]
exact this.comp continuous_quot_mk
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
[PROOFSTEP]
have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace :=
  by
  refine'
    unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap) (continuousSMul_induced φ.symm.toLinearMap)
      _
        -- Porting note: was `rw [t2Space_iff]`
  refine (@t2Space_iff 𝕜 (induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance)).mpr ?_
  exact fun x y hxy =>
    @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
      (φ.toEquiv.symm.injective.ne hxy)
        -- Finally, the pullback by `φ.symm` is exactly the pushforward by `φ`, so we have to prove
            -- that `φ` is continuous when `𝕜` is endowed with the pushforward by `φ` of the quotient
            -- topology, which is trivial by definition of the pushforward.
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
[PROOFSTEP]
refine'
  unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap) (continuousSMul_induced φ.symm.toLinearMap)
    _
      -- Porting note: was `rw [t2Space_iff]`
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ T2Space 𝕜
[PROOFSTEP]
refine (@t2Space_iff 𝕜 (induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance)).mpr ?_
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
⊢ ∀ (x y : 𝕜), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
[PROOFSTEP]
exact fun x y hxy =>
  @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _
    (φ.toEquiv.symm.injective.ne hxy)
      -- Finally, the pullback by `φ.symm` is exactly the pushforward by `φ`, so we have to prove
          -- that `φ` is continuous when `𝕜` is endowed with the pushforward by `φ` of the quotient
          -- topology, which is trivial by definition of the pushforward.
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
[PROOFSTEP]
rw [this.symm, Equiv.induced_symm]
[GOAL]
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'
l : E →ₗ[𝕜] 𝕜
hl : IsClosed ↑(ker l)
H : ¬finrank 𝕜 { x // x ∈ range l } = 0
this✝ : finrank 𝕜 { x // x ∈ range l } = 1
hi : Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
hs : Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
φ : (E ⧸ ker l) ≃ₗ[𝕜] 𝕜 :=
  LinearEquiv.ofBijective (Submodule.liftQ (ker l) l (_ : ker l ≤ ker l))
    (_ :
      Function.Injective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)) ∧
        Function.Surjective ↑(Submodule.liftQ (ker l) l (_ : ker l ≤ ker l)))
hlφ : ↑l = ↑φ ∘ ↑(Submodule.mkQ (ker l))
this : induced (↑(LinearEquiv.toEquiv φ).symm) inferInstance = UniformSpace.toTopologicalSpace
⊢ Continuous ↑(LinearEquiv.toEquiv φ)
[PROOFSTEP]
exact continuous_coinduced_rng
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₂ : Set.Nonempty s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
⊢ Continuous ↑l
[PROOFSTEP]
refine' l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => _)
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₂ : Set.Nonempty s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
hl : Dense ↑(ker l)
⊢ False
[PROOFSTEP]
rcases hs₂ with ⟨x, hx⟩
[GOAL]
case intro
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
hl : Dense ↑(ker l)
x : E
hx : x ∈ s
⊢ False
[PROOFSTEP]
have : x ∈ interior (LinearMap.ker l : Set E)ᶜ :=
  by
  rw [mem_interior_iff_mem_nhds]
  exact mem_of_superset (hs₁.mem_nhds hx) hs₃
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
hl : Dense ↑(ker l)
x : E
hx : x ∈ s
⊢ x ∈ interior (↑(ker l))ᶜ
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds]
[GOAL]
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
hl : Dense ↑(ker l)
x : E
hx : x ∈ s
⊢ (↑(ker l))ᶜ ∈ nhds x
[PROOFSTEP]
exact mem_of_superset (hs₁.mem_nhds hx) hs₃
[GOAL]
case intro
𝕜 : 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'
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen s
hs₃ : ∀ (x : E), x ∈ s → ↑l x ≠ 0
hl : Dense ↑(ker l)
x : E
hx : x ∈ s
this : x ∈ interior (↑(ker l))ᶜ
⊢ False
[PROOFSTEP]
rwa [hl.interior_compl] at this
[GOAL]
𝕜 : 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 ξ)
[PROOFSTEP]
letI : UniformSpace E := TopologicalAddGroup.toUniformSpace E
[GOAL]
𝕜 : 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 ξ)
[PROOFSTEP]
letI : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜 : 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 ξ)
[PROOFSTEP]
letI : SeparatedSpace E := separated_iff_t2.mpr ht2
[GOAL]
𝕜 : 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 ξ)
[PROOFSTEP]
induction' hn : Fintype.card ι with n IH generalizing ι E
[GOAL]
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 ξ)
[PROOFSTEP]
rw [Fintype.card_eq_zero_iff] at hn
[GOAL]
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 ξ)
[PROOFSTEP]
exact continuous_of_const fun x y => funext hn.elim
[GOAL]
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 ξ)
[PROOFSTEP]
haveI : FiniteDimensional 𝕜 E := of_fintype_basis ξ
[GOAL]
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 ξ)
[PROOFSTEP]
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
[GOAL]
𝕜 : 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
[PROOFSTEP]
intro s s_dim
[GOAL]
𝕜 : 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
[PROOFSTEP]
letI : UniformAddGroup s := s.toAddSubgroup.uniformAddGroup
[GOAL]
𝕜 : 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
[PROOFSTEP]
let b := Basis.ofVectorSpace 𝕜 s
[GOAL]
𝕜 : 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
[PROOFSTEP]
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
[GOAL]
𝕜 : 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)))
[PROOFSTEP]
have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n :=
  by
  rw [← s_dim]
  exact (finrank_eq_card_basis b).symm
[GOAL]
𝕜 : 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
[PROOFSTEP]
rw [← s_dim]
[GOAL]
𝕜 : 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 }
[PROOFSTEP]
exact (finrank_eq_card_basis b).symm
[GOAL]
𝕜 : 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)))
[PROOFSTEP]
have : Continuous b.equivFun := IH b this
[GOAL]
𝕜 : 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)))
[PROOFSTEP]
exact b.equivFun.symm.uniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
[GOAL]
𝕜 : 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
[PROOFSTEP]
have : IsComplete (s : Set E) := completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 (by infer_instance))
[GOAL]
𝕜 : 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 }) → 𝕜)
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : 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
[PROOFSTEP]
exact this.isClosed
[GOAL]
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 ξ)
[PROOFSTEP]
have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by
  intro f
  by_cases H : finrank 𝕜 (LinearMap.range f) = 0
  · rw [finrank_eq_zero, LinearMap.range_eq_bot] at H
    rw [H]
    exact continuous_zero
  · 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
    have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
    exact LinearMap.continuous_of_isClosed_ker f this
[GOAL]
𝕜 : 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
[PROOFSTEP]
intro f
[GOAL]
𝕜 : 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
[PROOFSTEP]
by_cases H : finrank 𝕜 (LinearMap.range f) = 0
[GOAL]
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
[PROOFSTEP]
rw [finrank_eq_zero, LinearMap.range_eq_bot] at H
[GOAL]
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
[PROOFSTEP]
rw [H]
[GOAL]
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
[PROOFSTEP]
exact continuous_zero
[GOAL]
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
[PROOFSTEP]
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
[GOAL]
𝕜 : 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
[PROOFSTEP]
have Z := f.finrank_range_add_finrank_ker
[GOAL]
𝕜 : 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
[PROOFSTEP]
rw [finrank_eq_card_basis ξ, hn] at Z
[GOAL]
𝕜 : 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
[PROOFSTEP]
have : finrank 𝕜 (LinearMap.range f) = 1 := le_antisymm (finrank_self 𝕜 ▸ f.range.finrank_le) (zero_lt_iff.mpr H)
[GOAL]
𝕜 : 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
[PROOFSTEP]
rw [this, add_comm, Nat.add_one] at Z
[GOAL]
𝕜 : 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
[PROOFSTEP]
exact Nat.succ.inj Z
[GOAL]
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
[PROOFSTEP]
have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
[GOAL]
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
[PROOFSTEP]
exact LinearMap.continuous_of_isClosed_ker f this
[GOAL]
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 ξ)
[PROOFSTEP]
rw [continuous_pi_iff]
[GOAL]
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
[PROOFSTEP]
intro i
[GOAL]
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
[PROOFSTEP]
change Continuous (ξ.coord i)
[GOAL]
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)
[PROOFSTEP]
exact H₂ (ξ.coord i)
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
⊢ Continuous ↑f
[PROOFSTEP]
let b := Basis.ofVectorSpace 𝕜 E
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
⊢ Continuous ↑f
[PROOFSTEP]
have A : Continuous b.equivFun := continuous_equivFun_basis_aux b
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
⊢ Continuous ↑f
[PROOFSTEP]
have B : Continuous (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E)) :=
  LinearMap.continuous_on_pi _
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
B : Continuous ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b)))
⊢ Continuous ↑f
[PROOFSTEP]
have : Continuous (f.comp (b.equivFun.symm : (Basis.ofVectorSpaceIndex 𝕜 E → 𝕜) →ₗ[𝕜] E) ∘ b.equivFun) := B.comp A
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
B : Continuous ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b)))
this : Continuous (↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b))
⊢ Continuous ↑f
[PROOFSTEP]
convert this
[GOAL]
case h.e'_5
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
B : Continuous ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b)))
this : Continuous (↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b))
⊢ ↑f = ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_5.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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
B : Continuous ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b)))
this : Continuous (↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b))
x : E
⊢ ↑f x = (↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b)) x
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_5.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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F'
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 E)) 𝕜 E := Basis.ofVectorSpace 𝕜 E
A : Continuous ↑(Basis.equivFun b)
B : Continuous ↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b)))
this : Continuous (↑(comp f ↑(LinearEquiv.symm (Basis.equivFun b))) ∘ ↑(Basis.equivFun b))
x : E
⊢ ↑f x = ↑f (↑(LinearEquiv.symm (Basis.equivFun (Basis.ofVectorSpace 𝕜 E))) ↑(↑(Basis.ofVectorSpace 𝕜 E).repr x))
[PROOFSTEP]
rw [Basis.equivFun_symm_apply, Basis.sum_repr]
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
⊢ IsOpenMap ↑f
[PROOFSTEP]
rcases f.exists_rightInverse_of_surjective (LinearMap.range_eq_top.2 hf) with ⟨g, hg⟩
[GOAL]
case intro
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
g : E →ₗ[𝕜] F
hg : comp f g = id
⊢ IsOpenMap ↑f
[PROOFSTEP]
refine' IsOpenMap.of_sections fun x => ⟨fun y => g (y - f x) + x, _, _, fun y => _⟩
[GOAL]
case intro.refine'_1
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
g : E →ₗ[𝕜] F
hg : comp f g = id
x : F
⊢ ContinuousAt (fun y => ↑g (y - ↑f x) + x) (↑f x)
[PROOFSTEP]
exact ((g.continuous_of_finiteDimensional.comp <| continuous_id.sub continuous_const).add continuous_const).continuousAt
[GOAL]
case intro.refine'_2
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
g : E →ₗ[𝕜] F
hg : comp f g = id
x : F
⊢ (fun y => ↑g (y - ↑f x) + x) (↑f x) = x
[PROOFSTEP]
simp only
[GOAL]
case intro.refine'_2
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
g : E →ₗ[𝕜] F
hg : comp f g = id
x : F
⊢ ↑g (↑f x - ↑f x) + x = x
[PROOFSTEP]
rw [sub_self, map_zero, zero_add]
[GOAL]
case intro.refine'_3
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : F →ₗ[𝕜] E
hf : Function.Surjective ↑f
g : E →ₗ[𝕜] F
hg : comp f g = id
x : F
y : E
⊢ ↑f ((fun y => ↑g (y - ↑f x) + x) y) = y
[PROOFSTEP]
simp only [map_sub, map_add, ← comp_apply f g, hg, id_apply, sub_add_cancel]
[GOAL]
𝕜 : 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 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (toContinuousLinearEquiv e).toLinearEquiv = e
[PROOFSTEP]
ext x
[GOAL]
case 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 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ ↑(toContinuousLinearEquiv e).toLinearEquiv x = ↑e x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : 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 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (ContinuousLinearEquiv.symm (toContinuousLinearEquiv e)).toLinearEquiv = symm e
[PROOFSTEP]
ext x
[GOAL]
case 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 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : F
⊢ ↑(ContinuousLinearEquiv.symm (toContinuousLinearEquiv e)).toLinearEquiv x = ↑(symm e) x
[PROOFSTEP]
rfl
[GOAL]
𝕜 : 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 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : T2Space E
v : Basis ι 𝕜 E
src✝ : E ≃ₗ[𝕜] ι → 𝕜 := equivFun v
⊢ Continuous
    { toLinearMap := ↑src✝, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.invFun
[PROOFSTEP]
change Continuous v.equivFun.symm.toFun
[GOAL]
𝕜 : 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 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : T2Space E
v : Basis ι 𝕜 E
src✝ : E ≃ₗ[𝕜] ι → 𝕜 := equivFun v
⊢ Continuous (↑(LinearEquiv.symm (equivFun v))).toAddHom.toFun
[PROOFSTEP]
exact v.equivFun.symm.toLinearMap.continuous_of_finiteDimensional
[GOAL]
𝕜 : 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : det f ≠ 0
⊢ ↑(toContinuousLinearEquivOfDetNeZero f hf) = f
[PROOFSTEP]
ext x
[GOAL]
case 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 𝕜
inst✝¹ : T2Space E
inst✝ : FiniteDimensional 𝕜 E
f : E →L[𝕜] E
hf : det f ≠ 0
x : E
⊢ ↑↑(toContinuousLinearEquivOfDetNeZero f hf) x = ↑f x
[PROOFSTEP]
rfl