Theorems · Definition · functional analysis

WithLp.linearEquiv

(p : ENNReal) →
  (K : Type u_1) →
    (V : Type u_4) → [inst : Semiring K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → WithLp p V ≃ₗ[K] V

WithLp.equiv as a linear equivalence.

Defined in

Mathlib.Analysis.Normed.Lp.WithLp

Cited by

29 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModule