Theorems · Theorem · functional analysis
enorm_ne_top
∀ {E : Type u_8} [inst : NNNorm E] {x : E}, ‖x‖ₑ ≠ ⊤- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 82 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NNNorm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Top.topstatement · cited by 9,680
- ENorm.enormstatement · cited by 715
- NNNormstatement and proof · cited by 33
Cited by82
Results whose statement or proof uses this declaration.
- MeasureTheory.memLp_constproof · cited by 16
- intervalIntegral.intervalIntegrable_cpow'proof · cited by 7
- MeasureTheory.memLp_top_constproof · cited by 6
- intervalIntegral.intervalIntegrable_rpow'proof · cited by 6
- MeasureTheory.measure_le_setAverage_posproof · cited by 5
- Real.GammaIntegral_convergentproof · cited by 5
- intervalIntegral.integral_deriv_smul_comp'''proof · cited by 4
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- sum_mul_eq_sub_sub_integral_mulproof · cited by 4
- MeasureTheory.locallyIntegrable_constproof · cited by 3
- Filter.Tendsto.integral_sub_linear_isLittleO_aeproof · cited by 3
- intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_leproof · cited by 3