Theorems · Theorem · functional analysis
norm_le_pi_norm
∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] (f : (i : ι) → G i)
(i : ι), ‖f i‖ ≤ ‖f‖- Cited by
- 17 results in Mathlib
- Foundations
- Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeSeminormedAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Fintypestatement and proof · cited by 7,736
- Norm.normstatement · cited by 5,413
- le_rflproof · cited by 1,558
- norm_nonnegproof · cited by 725
- SeminormedAddGroupstatement and proof · cited by 331
- pi_norm_le_iff_of_nonnegproof · cited by 18
Cited by17
Results whose statement or proof uses this declaration.
- ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_leproof · cited by 4
- MeasureTheory.HasFiniteIntegral.of_finiteproof · cited by 3
- MultilinearMap.norm_image_sub_le_of_boundproof · cited by 3
- IsUpperSet.exists_subset_ballproof · cited by 2
- IsLowerSet.exists_subset_ballproof · cited by 2
- ContinuousMultilinearMap.norm_iteratedFDerivComponent_leproof · cited by 1
- Matrix.norm_entry_le_entrywise_sup_normproof · cited by 1
- pi_norm_comp_leproof · cited by 1
- FormalMultilinearSeries.radius_pi_leproof · cited by 1
- nnnorm_le_pi_nnnormproof · cited by 1
- LinearIndependent.eventuallyproof · cited by 1
- Matrix.l2_opNorm_diagonalproof · cited by 1