Theorems · Definition · functional analysis

Module.Basis.equivFunL

{𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                [CompleteSpace 𝕜] → {ι : Type u_1} → [Finite ι] → [T2Space E] → Module.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 𝕜.

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

17 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceFiniteT2Space