Theorems · Theorem · functional analysis

WithLp.prodContinuousLinearEquiv_symm_apply

∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (x : α × β), (WithLp.prodContinuousLinearEquiv p 𝕜 α β).symm x = WithLp.toLp p x

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceSemiringAddCommGroupAddCommGroupModuleModule