Theorems · Definition · functional analysis

PiLp.continuousLinearEquiv

(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)] → PiLp p β ≃L[𝕜] (i : ι) → β i

WithLp.linearEquiv as a continuous linear equivalence.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

31 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModuleTopologicalSpace