Documentation

Mathlib.Topology.Algebra.Module.FiniteDimension

Finite dimensional topological vector spaces over complete fields #

Let π•œ be a complete nontrivially normed field, and E a topological vector space (TVS) over π•œ (i.e we have [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] and [ContinuousSMul π•œ E]).

If E is finite dimensional and Hausdorff, then all linear maps from E to any other TVS are continuous.

When E is a normed space, this gets us the equivalence of norms in finite dimension.

Main results : #

TODO #

Generalize more of Mathlib.Analysis.Normed.Module.FiniteDimension to general TVSs.

Implementation detail #

The main result from which everything follows is the fact that, if ΞΎ : ΞΉ β†’ E is a finite basis, then ΞΎ.equivFun : E β†’β‚— (ΞΉ β†’ π•œ) is continuous. However, for technical reasons, it is easier to prove this when ΞΉ and E live in the same universe. So we start by doing that as a private lemma, then we deduce LinearMap.continuous_of_finiteDimensional from it, and then the general result follows as continuous_equivFun_basis.

instance instFiniteDimensionalContinuousLinearMapId {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [Field π•œ] [TopologicalSpace π•œ] [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [FiniteDimensional π•œ E] [FiniteDimensional π•œ F] :
FiniteDimensional π•œ (E β†’L[π•œ] F)

The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.

Equations
  • β‹― = β‹―
theorem unique_topology_of_t2 {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {t : TopologicalSpace π•œ} (h₁ : TopologicalAddGroup π•œ) (hβ‚‚ : ContinuousSMul π•œ π•œ) (h₃ : T2Space π•œ) :
t = UniformSpace.toTopologicalSpace

If π•œ is a nontrivially normed field, any T2 topology on π•œ which makes it a topological vector space over itself (with the norm topology) is equal to the norm topology.

theorem LinearMap.continuous_of_isClosed_ker {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (l : E β†’β‚—[π•œ] π•œ) (hl : IsClosed ↑(LinearMap.ker l)) :
Continuous ⇑l

Any linear form on a topological vector space over a nontrivially normed field is continuous if its kernel is closed.

theorem LinearMap.continuous_iff_isClosed_ker {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (l : E β†’β‚—[π•œ] π•œ) :

Any linear form on a topological vector space over a nontrivially normed field is continuous if and only if its kernel is closed.

theorem LinearMap.continuous_of_nonzero_on_open {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] (l : E β†’β‚—[π•œ] π•œ) (s : Set E) (hs₁ : IsOpen s) (hsβ‚‚ : s.Nonempty) (hs₃ : βˆ€ x ∈ s, l x β‰  0) :
Continuous ⇑l

Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is automatically continuous.

theorem LinearMap.continuous_of_finiteDimensional {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
Continuous ⇑f

Any linear map on a finite dimensional space over a complete field is continuous.

instance LinearMap.continuousLinearMapClassOfFiniteDimensional {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] :
ContinuousLinearMapClass (E β†’β‚—[π•œ] F') π•œ E F'
Equations
  • β‹― = β‹―
theorem continuous_equivFun_basis {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] [T2Space E] {ΞΉ : Type u_1} [Finite ΞΉ] (ΞΎ : Basis ΞΉ π•œ E) :
Continuous ⇑ξ.equivFun

In finite dimensions over a non-discrete complete normed field, the canonical identification (in terms of a basis) with π•œ^n (endowed with the product topology) is continuous. This is the key fact which makes all linear maps from a T2 finite dimensional TVS over such a field continuous (see LinearMap.continuous_of_finiteDimensional), which in turn implies that all norms are equivalent in finite dimensions.

def LinearMap.toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] :
(E β†’β‚—[π•œ] F') ≃ₗ[π•œ] E β†’L[π•œ] F'

The continuous linear map induced by a linear map on a finite dimensional space

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Module.End.toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] [CompleteSpace π•œ] (E : Type v) [NormedAddCommGroup E] [NormedSpace π•œ E] [FiniteDimensional π•œ E] :
    (E β†’β‚—[π•œ] E) ≃ₐ[π•œ] E β†’L[π•œ] E

    Algebra equivalence between the linear maps and continuous linear maps on a finite dimensional space.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem LinearMap.coe_toContinuousLinearMap' {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
      ⇑(LinearMap.toContinuousLinearMap f) = ⇑f
      @[simp]
      theorem LinearMap.coe_toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
      ↑(LinearMap.toContinuousLinearMap f) = f
      @[simp]
      theorem LinearMap.coe_toContinuousLinearMap_symm {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] :
      ⇑LinearMap.toContinuousLinearMap.symm = ContinuousLinearMap.toLinearMap
      @[simp]
      theorem LinearMap.det_toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] E) :
      (LinearMap.toContinuousLinearMap f).det = LinearMap.det f
      @[simp]
      theorem LinearMap.ker_toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
      LinearMap.ker (LinearMap.toContinuousLinearMap f) = LinearMap.ker f
      @[simp]
      theorem LinearMap.range_toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F' : Type x} [AddCommGroup F'] [Module π•œ F'] [TopologicalSpace F'] [TopologicalAddGroup F'] [ContinuousSMul π•œ F'] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F') :
      LinearMap.range (LinearMap.toContinuousLinearMap f) = LinearMap.range f
      theorem LinearMap.isOpenMap_of_finiteDimensional {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : F β†’β‚—[π•œ] E) (hf : Function.Surjective ⇑f) :
      IsOpenMap ⇑f

      A surjective linear map f with finite dimensional codomain is an open map.

      instance LinearMap.canLiftContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] :
      CanLift (E β†’β‚—[π•œ] F) (E β†’L[π•œ] F) ContinuousLinearMap.toLinearMap fun (x : E β†’β‚—[π•œ] F) => True
      Equations
      • β‹― = β‹―
      def LinearEquiv.toContinuousLinearEquiv {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
      E ≃L[π•œ] F

      The continuous linear equivalence induced by a linear equivalence on a finite dimensional space.

      Equations
      • e.toContinuousLinearEquiv = { toLinearEquiv := e, continuous_toFun := β‹―, continuous_invFun := β‹― }
      Instances For
        @[simp]
        theorem LinearEquiv.coe_toContinuousLinearEquiv {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        ↑↑e.toContinuousLinearEquiv = ↑e
        @[simp]
        theorem LinearEquiv.coe_toContinuousLinearEquiv' {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        ⇑e.toContinuousLinearEquiv = ⇑e
        @[simp]
        theorem LinearEquiv.coe_toContinuousLinearEquiv_symm {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        ↑↑e.toContinuousLinearEquiv.symm = ↑e.symm
        @[simp]
        theorem LinearEquiv.coe_toContinuousLinearEquiv_symm' {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        ⇑e.toContinuousLinearEquiv.symm = ⇑e.symm
        @[simp]
        theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        e.toContinuousLinearEquiv.toLinearEquiv = e
        theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] (e : E ≃ₗ[π•œ] F) :
        e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm
        instance LinearEquiv.canLiftContinuousLinearEquiv {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] :
        CanLift (E ≃ₗ[π•œ] F) (E ≃L[π•œ] F) ContinuousLinearEquiv.toLinearEquiv fun (x : E ≃ₗ[π•œ] F) => True
        Equations
        • β‹― = β‹―
        theorem FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] [FiniteDimensional π•œ F] (cond : Module.finrank π•œ E = Module.finrank π•œ F) :
        Nonempty (E ≃L[π•œ] F)

        Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if they have the same (finite) dimension.

        theorem FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] [FiniteDimensional π•œ F] :
        Nonempty (E ≃L[π•œ] F) ↔ Module.finrank π•œ E = Module.finrank π•œ F

        Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if and only if they have the same (finite) dimension.

        def ContinuousLinearEquiv.ofFinrankEq {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] [T2Space F] [FiniteDimensional π•œ E] [FiniteDimensional π•œ F] (cond : Module.finrank π•œ E = Module.finrank π•œ F) :
        E ≃L[π•œ] F

        A continuous linear equivalence between two finite-dimensional topological vector spaces over a complete normed field of the same (finite) dimension.

        Equations
        Instances For
          def Basis.constrL {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) (f : ΞΉ β†’ F) :
          E β†’L[π•œ] F

          Construct a continuous linear map given the value at a finite basis.

          Equations
          • v.constrL f = LinearMap.toContinuousLinearMap ((v.constr π•œ) f)
          Instances For
            @[simp]
            theorem Basis.coe_constrL {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) (f : ΞΉ β†’ F) :
            ↑(v.constrL f) = (v.constr π•œ) f
            @[simp]
            theorem Basis.equivFunL_apply {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) :
            βˆ€ (a : E) (a_1 : ΞΉ), v.equivFunL a a_1 = (v.repr a) a_1
            def Basis.equivFunL {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) :
            E ≃L[π•œ] ΞΉ β†’ π•œ

            The continuous linear equivalence between a vector space over π•œ with a finite basis and functions from its basis indexing type to π•œ.

            Equations
            • v.equivFunL = { toLinearEquiv := v.equivFun, continuous_toFun := β‹―, continuous_invFun := β‹― }
            Instances For
              @[simp]
              theorem Basis.equivFunL_symm_apply_repr {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) (x : E) :
              v.equivFunL.symm ⇑(v.repr x) = x
              @[simp]
              theorem Basis.constrL_apply {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] [T2Space E] {ΞΉ : Type u_2} [Fintype ΞΉ] (v : Basis ΞΉ π•œ E) (f : ΞΉ β†’ F) (e : E) :
              (v.constrL f) e = βˆ‘ i : ΞΉ, v.equivFun e i β€’ f i
              @[simp]
              theorem Basis.constrL_basis {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] {F : Type w} [AddCommGroup F] [Module π•œ F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] [T2Space E] (v : Basis ΞΉ π•œ E) (f : ΞΉ β†’ F) (i : ΞΉ) :
              (v.constrL f) (v i) = f i
              def ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’L[π•œ] E) (hf : f.det β‰  0) :
              E ≃L[π•œ] E

              Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional vector space whose determinant is nonzero.

              Equations
              • f.toContinuousLinearEquivOfDetNeZero hf = ((↑f).equivOfDetNeZero hf).toContinuousLinearEquiv
              Instances For
                @[simp]
                theorem ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’L[π•œ] E) (hf : f.det β‰  0) :
                ↑(f.toContinuousLinearEquivOfDetNeZero hf) = f
                @[simp]
                theorem ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] {E : Type v} [AddCommGroup E] [Module π•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul π•œ E] [CompleteSpace π•œ] [T2Space E] [FiniteDimensional π•œ E] (f : E β†’L[π•œ] E) (hf : f.det β‰  0) (x : E) :
                (f.toContinuousLinearEquivOfDetNeZero hf) x = f x
                theorem Matrix.toLin_finTwoProd_toContinuousLinearMap {π•œ : Type u} [hnorm : NontriviallyNormedField π•œ] [CompleteSpace π•œ] (a : π•œ) (b : π•œ) (c : π•œ) (d : π•œ) :
                LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd π•œ) (Basis.finTwoProd π•œ)) !![a, b; c, d]) = (a β€’ ContinuousLinearMap.fst π•œ π•œ π•œ + b β€’ ContinuousLinearMap.snd π•œ π•œ π•œ).prod (c β€’ ContinuousLinearMap.fst π•œ π•œ π•œ + d β€’ ContinuousLinearMap.snd π•œ π•œ π•œ)
                theorem FiniteDimensional.complete (π•œ : Type u_1) (E : Type u_2) [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [UniformSpace E] [T2Space E] [UniformAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [FiniteDimensional π•œ E] :
                theorem Submodule.complete_of_finiteDimensional {π•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [UniformSpace E] [T2Space E] [UniformAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] (s : Submodule π•œ E) [FiniteDimensional π•œ β†₯s] :
                IsComplete ↑s

                A finite-dimensional subspace is complete.

                theorem Submodule.closed_of_finiteDimensional {π•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [T2Space E] (s : Submodule π•œ E) [FiniteDimensional π•œ β†₯s] :
                IsClosed ↑s

                A finite-dimensional subspace is closed.

                theorem LinearMap.closedEmbedding_of_injective {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [AddCommGroup F] [TopologicalSpace F] [T2Space F] [TopologicalAddGroup F] [Module π•œ F] [ContinuousSMul π•œ F] [T2Space E] [FiniteDimensional π•œ E] {f : E β†’β‚—[π•œ] F} (hf : LinearMap.ker f = βŠ₯) :

                An injective linear map with finite-dimensional domain is a closed embedding.

                theorem closedEmbedding_smul_left {π•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [T2Space E] {c : E} (hc : c β‰  0) :
                ClosedEmbedding fun (x : π•œ) => x β€’ c
                theorem isClosedMap_smul_left {π•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [T2Space E] (c : E) :
                IsClosedMap fun (x : π•œ) => x β€’ c
                theorem ContinuousLinearMap.exists_right_inverse_of_surjective {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField π•œ] [CompleteSpace π•œ] [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [Module π•œ E] [ContinuousSMul π•œ E] [AddCommGroup F] [TopologicalSpace F] [T2Space F] [TopologicalAddGroup F] [Module π•œ F] [ContinuousSMul π•œ F] [FiniteDimensional π•œ F] (f : E β†’L[π•œ] F) (hf : LinearMap.range f = ⊀) :
                βˆƒ (g : F β†’L[π•œ] E), f.comp g = ContinuousLinearMap.id π•œ F