Theorems · Theorem · functional analysis
PiLp.edist_single_same
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
[inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
edist (PiLp.single p i b₁) (PiLp.single p i b₂) = edist b₁ b₂- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 224 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Fintypestatement and proof · cited by 7,736
- Factstatement and proof · cited by 2,726
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- ENNReal.ofNNRealproof · cited by 1,279
- EDist.ediststatement · cited by 735
- NNDist.nndistproof · cited by 235
- PiLpstatement · cited by 150
- edist_nndistproof · cited by 38
- PiLp.singlestatement and proof · cited by 24
- PiLp.nndist_single_sameproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- EuclideanSpace.edist_single_sameproof · cited by 0
- PiLp.edist_toLp_single_sameproof · cited by 0