Theorems · Definition · functional analysis

LinearMap.toContinuousLinearMap

{𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F' : Type x} →
                  [inst_5 : AddCommGroup F'] →
                    [inst_6 : Module 𝕜 F'] →
                      [inst_7 : TopologicalSpace F'] →
                        [inst_8 : IsTopologicalAddGroup F'] →
                          [inst_9 : 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

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

43 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceT2SpaceFiniteDimensional