∀ (p : ENNReal) {ι : Type u_1} (β : ι → Type u_2) [inst : Fact (1 ≤ p)] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
  [inst_2 : Fintype ι], uniformity (PiLp p β) = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p_1 | edist p_1.1 p_1.2 < ε}