Theorems · Theorem · functional analysis
WithLp.nnnorm_snd_le
∀ {p : ENNReal} (α : Type u_2) {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
[inst_1 : SeminormedAddCommGroup β] (x : WithLp p (α × β)), ‖x.snd‖₊ ≤ ‖x‖₊- Defined in
- Mathlib.Analysis.Normed.Lp.ProdLp
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- NNRealstatement · cited by 4,310
- Factstatement and proof · cited by 2,726
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- NNNorm.nnnormstatement · cited by 952
- WithLpstatement and proof · cited by 345
- WithLp.sndstatement and proof · cited by 76
- nndist_zero_rightproof · cited by 4
- WithLp.nndist_snd_leproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.