Theorems · Definition · functional analysis

LinearEquiv.toContinuousLinearEquiv

{𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F : Type w} →
                  [inst_5 : AddCommGroup F] →
                    [inst_6 : Module 𝕜 F] →
                      [inst_7 : TopologicalSpace F] →
                        [IsTopologicalAddGroup F] →
                          [ContinuousSMul 𝕜 F] →
                            [CompleteSpace 𝕜] →
                              [T2Space E] → [T2Space F] → [FiniteDimensional 𝕜 E] → (E ≃ₗ[𝕜] F) → E ≃L[𝕜] F

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

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

25 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceT2SpaceT2SpaceFiniteDimensional