𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
f : E →ₗ[𝕜] F
hf : LinearMap.ker f = ⊥
inst✝ : FiniteDimensional 𝕜 E
g : E ≃ₗ[𝕜] { x // x ∈ LinearMap.range f } := ofInjective f (_ : Function.Injective ↑f)
src✝ : Embedding (Subtype.val ∘ ↑(ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g))) :=
  Embedding.comp embedding_subtype_val
    (Homeomorph.embedding (ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g)))
this : FiniteDimensional 𝕜 { x // x ∈ LinearMap.range f }
⊢ IsClosed (range ↑f)
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
f : E →ₗ[𝕜] F
hf : LinearMap.ker f = ⊥
inst✝ : FiniteDimensional 𝕜 E
g : E ≃ₗ[𝕜] { x // x ∈ LinearMap.range f } := ofInjective f (_ : Function.Injective ↑f)
src✝ : Embedding (Subtype.val ∘ ↑(ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g))) :=
  Embedding.comp embedding_subtype_val
    (Homeomorph.embedding (ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g)))
⊢ IsClosed (range ↑f)
haveI := f.finiteDimensional_range
no goals
𝕜 : Type u
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type w
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
F' : Type x
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module 𝕜 F'
inst✝⁴ : TopologicalSpace F'
inst✝³ : TopologicalAddGroup F'
inst✝² : ContinuousSMul 𝕜 F'
inst✝¹ : CompleteSpace 𝕜
f : E →ₗ[𝕜] F
hf : LinearMap.ker f = ⊥
inst✝ : FiniteDimensional 𝕜 E
g : E ≃ₗ[𝕜] { x // x ∈ LinearMap.range f } := ofInjective f (_ : Function.Injective ↑f)
src✝ : Embedding (Subtype.val ∘ ↑(ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g))) :=
  Embedding.comp embedding_subtype_val
    (Homeomorph.embedding (ContinuousLinearEquiv.toHomeomorph (toContinuousLinearEquiv g)))
this : FiniteDimensional 𝕜 { x // x ∈ LinearMap.range f }
⊢ IsClosed (range ↑f)
simpa [LinearMap.range_coe f] using f.range.closed_of_finiteDimensional