Theorems · Theorem · real analysis
ENNReal.ofNat_ne_top
∀ {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n ≠ ⊤- Defined in
- Mathlib.Data.ENNReal.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Nat.AtLeastTwo
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
- Nat.AtLeastTwostatement and proof · cited by 405
- ENNReal.natCast_ne_topproof · cited by 11
Cited by29
Results whose statement or proof uses this declaration.
- ENNReal.half_posproof · cited by 13
- MeasureTheory.TendstoInMeasure.exists_seq_tendsto_aeproof · cited by 5
- MeasureTheory.MemLp.integrable_sqproof · cited by 5
- ProbabilityTheory.evariance_lt_topproof · cited by 3
- ENNReal.rpow_add_le_mul_rpow_add_rpowproof · cited by 3
- NumberField.mixedEmbedding.fundamentalCone.volume_normLeOneproof · cited by 2
- ProbabilityTheory.evariance_eq_topproof · cited by 2
- MeasureTheory.Lp.fourier_toTemperedDistribution_eqproof · cited by 2
- ExpGrowth.expGrowthSup_addproof · cited by 2
- MeasureTheory.tendsto_lintegral_norm_of_dominated_convergenceproof · cited by 2
- ENNReal.LpAddConst_lt_topproof · cited by 2