Theorems · Theorem · functional analysis
BoundedContinuousFunction.norm_coe_le_norm
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
(f : BoundedContinuousFunction α β) (x : α), ‖f x‖ ≤ ‖f‖- Cited by
- 25 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- Norm.normstatement and proof · cited by 5,413
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- BoundedContinuousFunctionstatement and proof · cited by 511
- dist_zero_rightproof · cited by 172
- BoundedContinuousFunction.dist_coe_le_distproof · cited by 18
Cited by25
Results whose statement or proof uses this declaration.
- ContinuousMap.norm_coe_le_normproof · cited by 14
- ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminormproof · cited by 5
- indicator_indepFun_pi_of_prod_bcfproof · cited by 4
- BoundedContinuousFunction.mem_Lpproof · cited by 4
- isCompact_setOfPred_finiteMeasure_le_of_compactSpaceproof · cited by 3
- isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_leproof · cited by 2
- BoundedContinuousFunction.norm_sub_nonnegproof · cited by 2
- BoundedContinuousFunction.add_norm_nonnegproof · cited by 2
- summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexpproof · cited by 2
- BoundedContinuousFunction.dist_le_two_normproof · cited by 2
- BoundedContinuousFunction.exists_norm_eq_domRestrict_eqproof · cited by 1
- BoundedContinuousFunction.Lp_nnnorm_leproof · cited by 1