Theorems · Theorem · functional analysis

IsometryEquiv.withLpProdUnique_symm_apply

∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique β] (a : α),
  (IsometryEquiv.withLpProdUnique p α β).symm a = WithLp.toLp p (a, default)

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactPseudoEMetricSpacePseudoEMetricSpaceUnique