Theorems · Definition · functional analysis

IsometryEquiv.withLpProdUnique

(p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) →
      [hp : Fact (1 ≤ p)] →
        [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → [Unique β] → WithLp p (α × β) ≃ᵢ α

Right identity of the L^p product as an isometric equivalence.

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

FactPseudoEMetricSpacePseudoEMetricSpaceUnique