Mathlib Map

Theorems · Definition · order theory

ENat.toENNReal

ℕ∞ → ENNReal

Coercion from ℕ∞ to ℝ≥0∞.

Defined in
Mathlib.Data.Real.ENatENNReal
Cited by
103 results in Mathlib
Foundations
Depth 110 from the axioms, rests on 2,148 definitions · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ENat.toENNReal_mono · cited by 25ENat.toENNReal_monoDynamics.coverEntropyEntourage · cited by 20Dynamics.coverEntropyEnto…Dynamics.coverEntropyInfEntourage · cited by 15Dynamics.coverEntropyInfE…ENat.toENNReal_one · cited by 12ENat.toENNReal_oneDynamics.netEntropyEntourage · cited by 11Dynamics.netEntropyEntour…Dynamics.netEntropyInfEntourage · cited by 11Dynamics.netEntropyInfEnt…ENat.toENNReal_zero · cited by 9ENat.toENNReal_zeroDynamics.coverEntropyEntourage_antitone · cited by 6Dynamics.coverEntropyEnto…Dynamics.coverEntropyInfEntourage_antitone · cited by 4Dynamics.coverEntropyInfE…MeasureTheory.Measure.count_apply_finset' · cited by 4Measure.count_apply_finse…MeasureTheory.Measure.count_univ · cited by 4Measure.count_univENat.ceil_le · cited by 4ENat.ceil_leMeasureTheory.Measure.count_apply · cited by 3Measure.count_applyENat.ceil_natCast · cited by 3ENat.ceil_natCastENat.ceil_sub_toENNReal · cited by 3ENat.ceil_sub_toENNRealENNReal · cited by 9879ENNRealENat · cited by 4985ENatENat.map · cited by 31ENat.mapENat.toENNRealCITED BYCITES

Cites3

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

Cited by107

Results whose statement or proof uses this declaration.