Theorems · Definition · functional analysis

IsometryEquiv.withLpProdComm

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

Commutativity of the L^p product as an isometric equivalence.

Defined in: Mathlib.Analysis.Normed.Lp.ProdLp
Cited by: 2 results in Mathlib
Foundations: Depth 220 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact PseudoEMetricSpace PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

ENNRealstatement and proof · cited by 9,879
Equivproof · cited by 8,337
Factstatement and proof · cited by 2,726
PseudoEMetricSpacestatement and proof · cited by 1,536
WithLpstatement and proof · cited by 345
IsometryEquivstatement · cited by 177
Equiv.prodCommproof · cited by 55
WithLp.congrproof · cited by 4

Cited by3

Results whose statement or proof uses this declaration.

IsometryEquiv.withLpUniqueProdproof · cited by 3
IsometryEquiv.withLpProdComm_symmstatement · cited by 0
IsometryEquiv.withLpProdComm_applystatement · cited by 0