Theorems · Theorem · functional analysis
PiLp.lipschitzWith_toLp
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
[inst_1 : (i : ι) → PseudoEMetricSpace (β i)], LipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) (WithLp.toLp p)- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 220 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- NNRealstatement · cited by 4,310
- Factstatement and proof · cited by 2,726
- PseudoEMetricSpacestatement and proof · cited by 1,536
- Fintype.cardstatement · cited by 1,386
- ENNReal.toRealstatement · cited by 859
- WithLpstatement · cited by 345
- LipschitzWithstatement · cited by 316
- WithLp.ofLp_toLpproof · cited by 7
- PiLp.antilipschitzWith_ofLpproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- PiLp.isUniformInducing_toLpproof · cited by 0