Theorems · Theorem · functional analysis
WithLp.isBoundedSMulSeminormedAddCommGroupToProd
∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : SeminormedAddCommGroup α]
[inst_1 : SeminormedAddCommGroup β] {R : Type u_6} [inst_2 : SeminormedRing R] [inst_3 : Module R α]
[inst_4 : Module R β] [IsBoundedSMul R α] [IsBoundedSMul R β], IsBoundedSMul R (α × β)- Defined in
- Mathlib.Analysis.Normed.Lp.ProdLp
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 225 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Modulestatement and proof · cited by 20,661
- ENNRealstatement and proof · cited by 9,879
- Factstatement and proof · cited by 2,726
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- PseudoMetricSpaceproof · cited by 1,550
- Dist.distproof · cited by 1,539
- SeminormedRingstatement and proof · cited by 446
- IsBoundedSMulstatement and proof · cited by 329
- dist_zero_rightproof · cited by 172
- dist_smul_pairproof · cited by 5
- dist_pair_smulproof · cited by 4
- WithLp.pseudoMetricSpaceToProdstatement and proof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.