Mathlib Map

Theorems · Theorem · real analysis

NNReal.coe_pos

∀ {r : NNReal}, 0 < ↑r ↔ 0 < r
Defined in
Mathlib.Data.NNReal.Defs
Cited by
31 results in Mathlib
Foundations
Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib.Meta.Positivity.nnreal_coe_pos · cited by 31Positivity.nnreal_coe_posENNReal.toReal_pos_iff · cited by 20ENNReal.toReal_pos_iffAsymptotics.isLittleOTVS_iff_isLittleO · cited by 7Asymptotics.isLittleOTVS_…NNReal.rpow_add · cited by 4NNReal.rpow_addFormalMultilinearSeries.div_le_radius_compContinuousLinearMap · cited by 3FormalMultilinearSeries.d…Metric.cthickening_eq_iInter_cthickening' · cited by 3Metric.cthickening_eq_iIn…HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal · cited by 3HasFPowerSeriesWithinOnBa…cauchySeq_of_edist_le_of_summable · cited by 2cauchySeq_of_edist_le_of_…Seminorm.finset_sup_apply_lt · cited by 2Seminorm.finset_sup_apply…HolderOnWith.of_le · cited by 2HolderOnWith.of_leStieltjesFunction.outer_Ioc · cited by 2StieltjesFunction.outer_I…AntilipschitzWith.add_lipschitzWith · cited by 2AntilipschitzWith.add_lip…MeasureTheory.IntegrableOn.hasBoxIntegral · cited by 2IntegrableOn.hasBoxIntegr…Disjoint.exists_thickenings · cited by 1Disjoint.exists_thickenin…BoxIntegral.hasIntegralIndicatorConst · cited by 1BoxIntegral.hasIntegralIn…Real · cited by 25697RealNNReal · cited by 4310NNRealNNReal.toReal · cited by 1260NNReal.toRealNNReal.coe_posCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement · cited by 25,697
  • NNRealstatement and proof · cited by 4,310
  • NNReal.toRealstatement · cited by 1,260

Cited by31

Results whose statement or proof uses this declaration.