Theorems · Definition · functional analysis

WithLp.pseudoMetricSpaceToProd

(p : ENNReal) →
  [hp : Fact (1 ≤ p)] →
    (α : Type u_4) → (β : Type u_5) → [PseudoMetricSpace α] → [PseudoMetricSpace β] → PseudoMetricSpace (α × β)

This definition allows to endow α × β with the Lp distance with the uniformity and bornology being defeq to the product ones. It is useful to endow a type synonym of a × β with the Lp distance.

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactPseudoMetricSpacePseudoMetricSpace