Theorems · Definition · functional analysis

PiLp.equivOfUnique

(p : ENNReal) →
  (𝕜 : Type u_1) →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [inst : Semiring 𝕜] →
          [inst_1 : (i : ι) → AddCommGroup (β i)] →
            [inst_2 : (i : ι) → Module 𝕜 (β i)] →
              [inst_3 : (i : ι) → TopologicalSpace (β i)] → [inst_4 : Unique ι] → PiLp p β ≃L[𝕜] β default

The natural equivalence between PiLp p β and β default, for any index type ι with a unique element.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModuleTopologicalSpaceUnique