Theorems · Definition · functional analysis

ContinuousLinearEquiv.ofFinrankEq

{𝕜 : 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] →
                                    [FiniteDimensional 𝕜 F] → 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.

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

10 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceT2SpaceT2SpaceFiniteDimensionalFiniteDimensional