Theorems · Definition · functional analysis

PiLp.pseudoEmetricAux

(p : ENNReal) →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [Fact (1 ≤ p)] → [(i : ι) → PseudoEMetricSpace (β i)] → [Fintype ι] → PseudoEMetricSpace (PiLp p β)

Endowing the space PiLp p β with the L^p pseudoemetric structure. This definition is not satisfactory, as it does not register the fact that the topology and the uniform structure coincide with the product one. Therefore, we do not register it as an instance. Using this as a temporary pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to the product one, and then register an instance in which we replace the uniform structure by the product one using this pseudoemetric space and PseudoEMetricSpace.replaceUniformity.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactPseudoEMetricSpaceFintype