Mathlib Map

Theorems · Theorem · real analysis

ENNReal.ofReal_zero

ENNReal.ofReal 0 = 0
Defined in
Mathlib.Data.ENNReal.Basic
Cited by
56 results in Mathlib
Foundations
Depth 110 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.

Real.Gamma_pos_of_pos · cited by 17Real.Gamma_pos_of_posENNReal.ofReal_rpow_of_nonneg · cited by 13ENNReal.ofReal_rpow_of_no…MeasureTheory.Measure.addHaar_smul · cited by 13Measure.addHaar_smulMeasureTheory.tilted_zero_measure · cited by 12MeasureTheory.tilted_zero…StieltjesFunction.measure_singleton · cited by 6StieltjesFunction.measure…EReal.continuous_toENNReal · cited by 4EReal.continuous_toENNRealReal.ediam_eq · cited by 4Real.ediam_eqMeasureTheory.Measure.addHaar_image_linearMap · cited by 4Measure.addHaar_image_lin…InformationTheory.klDiv_self · cited by 4InformationTheory.klDiv_s…StieltjesFunction.length_empty · cited by 3StieltjesFunction.length_…MeasureTheory.tilted_of_not_integrable · cited by 3MeasureTheory.tilted_of_n…MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top · cited by 3MeasureTheory.hasFiniteIn…MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn · cited by 3MeasureTheory.lintegral_i…Metric.exists_forall_closedEBall_subset_aux₁ · cited by 3Metric.exists_forall_clos…HasConstantSpeedOnWith.union · cited by 2HasConstantSpeedOnWith.un…Real · cited by 25697RealENNReal · cited by 9879ENNRealENNReal.ofNNReal · cited by 1279ENNReal.ofNNRealENNReal.ofReal · cited by 863ENNReal.ofRealReal.toNNReal_zero · cited by 9Real.toNNReal_zeroENNReal.ofReal_zeroCITED BYCITES

Cites5

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

Cited by56

Results whose statement or proof uses this declaration.