Mathlib Map

Theorems · Definition · real analysis

ENNReal.ofReal

ℝ → ENNReal

ofReal x returns x if it is nonnegative, 0 otherwise.

Defined in
Mathlib.Data.ENNReal.Basic
Cited by
863 results in Mathlib
Foundations
Depth 108 from the axioms, rests on 2,180 definitions · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Metric.thickening · cited by 130Metric.thickeningMetric.cthickening · cited by 113Metric.cthickeningENNReal.toReal_ofReal · cited by 82ENNReal.toReal_ofRealENNReal.ofReal_toReal · cited by 65ENNReal.ofReal_toRealENNReal.ofReal_le_ofReal · cited by 61ENNReal.ofReal_le_ofRealENNReal.ofReal_one · cited by 61ENNReal.ofReal_oneMeasureTheory.Measure.tilted · cited by 58Measure.tiltedENNReal.ofReal_zero · cited by 56ENNReal.ofReal_zeroENNReal.ofReal_coe_nnreal · cited by 52ENNReal.ofReal_coe_nnrealEReal.exp · cited by 46EReal.expENNReal.ofReal_mul · cited by 44ENNReal.ofReal_muledist_dist · cited by 39edist_distofReal_norm · cited by 39ofReal_normedist_nndist · cited by 38edist_nndistedist_eq_enorm_sub · cited by 37edist_eq_enorm_subReal · cited by 25697RealENNReal · cited by 9879ENNRealENNReal.ofNNReal · cited by 1279ENNReal.ofNNRealReal.toNNReal · cited by 267Real.toNNRealENNReal.ofRealCITED BYCITES

Cites4

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

Cited by894

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 894.