Theorems · Theorem · functional analysis
PiLp.edist_comm
∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
(f g : PiLp p β), edist f g = edist g fThis holds independent of p and does not require [Fact (1 ≤ p)]. We keep it separate
from pi_Lp.pseudo_emetric_space so it can be used also for p < 1.
- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypePseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites22
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
- Top.topproof · cited by 9,680
- Fintypestatement and proof · cited by 7,736
- Set.ofPredproof · cited by 6,101
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- iSupproof · cited by 2,415
- Finset.cardproof · cited by 2,327
- Finset.sum_congrproof · cited by 2,323
- PseudoEMetricSpacestatement and proof · cited by 1,536
- ENNReal.toRealproof · cited by 859
- EDist.ediststatement and proof · cited by 735
Cited by1
Results whose statement or proof uses this declaration.
- PiLp.pseudoEmetricAuxproof · cited by 0