Theorems · Definition · functional analysis

toEuclidean

{E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : TopologicalSpace E] →
      [IsTopologicalAddGroup E] →
        [T2Space E] →
          [inst_4 : Module ℝ E] →
            [ContinuousSMul ℝ E] → [FiniteDimensional ℝ E] → E ≃L[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ E))

If E is a finite-dimensional space over ℝ, then toEuclidean is a continuous ℝ-linear equivalence between E and the Euclidean space of the same dimension.

Defined in

Mathlib.Analysis.InnerProductSpace.EuclideanDist

Cited by

16 results in Mathlib

Foundations

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

Assumes

AddCommGroupTopologicalSpaceIsTopologicalAddGroupT2SpaceModuleContinuousSMulFiniteDimensional