Mathlib Map

Theorems · Theorem · real analysis

ENNReal.coe_le_coe

∀ {r q : NNReal}, ↑r ≤ ↑q ↔ r ≤ q
Defined in
Mathlib.Data.ENNReal.Basic
Cited by
73 results in Mathlib
Foundations
Depth 107 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.

ENNReal.ofReal_le_ofReal_iff · cited by 20ENNReal.ofReal_le_ofReal_…BoundedContinuousFunction.lintegral_lt_top_of_nnreal · cited by 11BoundedContinuousFunction…ENNReal.coe_mono · cited by 10ENNReal.coe_monoegauge_ball_le_of_one_lt_norm · cited by 4egauge_ball_le_of_one_lt_…ENNReal.ofReal_add_le · cited by 4ENNReal.ofReal_add_leENNReal.toNNReal_le_toNNReal · cited by 4ENNReal.toNNReal_le_toNNR…LipschitzWith.weaken · cited by 4LipschitzWith.weakenHolderOnWith.nndist_le_of_le · cited by 3HolderOnWith.nndist_le_of…MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound · cited by 3MeasureTheory.eLpNormEssS…FormalMultilinearSeries.ofScalars_radius_eq_inv_of_tendsto · cited by 3FormalMultilinearSeries.o…enorm_sub_le · cited by 3enorm_sub_leENNReal.coe_inv_le · cited by 3ENNReal.coe_inv_leisCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le · cited by 2isCompact_setOfPred_finit…NonUnitalStarAlgHom.nnnorm_apply_le · cited by 2NonUnitalStarAlgHom.nnnor…MeasureTheory.setLIntegral_lt_top_of_bddAbove · cited by 2MeasureTheory.setLIntegra…ENNReal · cited by 9879ENNRealNNReal · cited by 4310NNRealENNReal.ofNNReal · cited by 1279ENNReal.ofNNRealWithTop.coe_le_coe · cited by 65WithTop.coe_le_coeENNReal.coe_le_coeCITED BYCITES

Cites4

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

Cited by73

Results whose statement or proof uses this declaration.