Theorems · Theorem · functional analysis
PiLp.isUniformInducing_toLp
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [Finite ι]
[inst : (i : ι) → PseudoEMetricSpace (β i)], IsUniformInducing (WithLp.toLp p)- Defined in
- Mathlib.Analysis.Normed.Lp.PiLp
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FactFinitePseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- Fintypeproof · cited by 7,736
- Finitestatement and proof · cited by 3,029
- Factstatement and proof · cited by 2,726
- PseudoEMetricSpacestatement and proof · cited by 1,536
- WithLpstatement · cited by 345
- Fintype.ofFiniteproof · cited by 255
- IsUniformInducingstatement · cited by 128
- LipschitzWith.uniformContinuousproof · cited by 33
- AntilipschitzWith.isUniformInducingproof · cited by 8
- PiLp.antilipschitzWith_toLpproof · cited by 1
- PiLp.lipschitzWith_toLpproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.