Mathlib Map

Theorems · Theorem · real analysis

ENNReal.lt_iff_exists_nnreal_btwn

∀ {a b : ENNReal}, a < b ↔ ∃ r, a < ↑r ∧ ↑r < b
Defined in
Mathlib.Data.ENNReal.Basic
Cited by
17 results in Mathlib
Foundations
Depth 111 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.

hausdorffMeasure_of_dimH_lt · cited by 5hausdorffMeasure_of_dimH_…ENNReal.lt_iff_exists_add_pos_lt · cited by 3ENNReal.lt_iff_exists_add…Metric.exists_pos_forall_lt_edist · cited by 2Metric.exists_pos_forall_…HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub · cited by 2HasFPowerSeriesWithinAt.i…Metric.eventually_nhds_zero_forall_closedEBall_subset · cited by 2Metric.eventually_nhds_ze…HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn · cited by 2HasFPowerSeriesWithinOnBa…HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod · cited by 2HasFPowerSeriesWithinOnBa…FormalMultilinearSeries.comp_summable_nnreal · cited by 2FormalMultilinearSeries.c…HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow · cited by 1HasFPowerSeriesWithinAt.i…Metric.uniformity_edist_aux · cited by 1Metric.uniformity_edist_a…uniformity_basis_edist_nnreal · cited by 1uniformity_basis_edist_nn…Metric.secondCountable_of_almost_dense_set · cited by 1Metric.secondCountable_of…ENNReal.tendsto_mul · cited by 1ENNReal.tendsto_mulVitaliFamily.ae_eventually_measure_zero_of_singular · cited by 1VitaliFamily.ae_eventuall…FormalMultilinearSeries.le_mul_pow_of_radius_pos · cited by 1FormalMultilinearSeries.l…ENNReal · cited by 9879ENNRealNNReal · cited by 4310NNRealENNReal.ofNNReal · cited by 1279ENNReal.ofNNRealWithTop.lt_iff_exists_coe_btwn · cited by 1WithTop.lt_iff_exists_coe…ENNReal.lt_iff_exists_nnreal_…CITED BYCITES

Cites4

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

Cited by17

Results whose statement or proof uses this declaration.