Theorems · Definition · measure theory

OrthonormalBasis.measurableEquiv

{ι : Type u_1} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [inst_1 : InnerProductSpace ℝ F] →
        [inst_2 : MeasurableSpace F] →
          [BorelSpace F] → [inst_4 : Fintype ι] → OrthonormalBasis ι ℝ F → F ≃ᵐ EuclideanSpace ℝ ι

An orthonormal basis of a finite-dimensional inner product space defines a measurable equivalence between the space and the Euclidean space of the same dimension.

Defined in

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFintype