Theorems · Theorem · real analysis
ENNReal.div_lt_iff
∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ 0 → b ≠ ⊤ ∨ c ≠ ⊤ → (c / b < a ↔ c < a * b)- Defined in
- Mathlib.Data.ENNReal.Inv
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- lt_iff_lt_of_le_iff_leproof · cited by 54
- ENNReal.le_div_iff_mul_leproof · cited by 15
Cited by10
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Fernique.logRatio_posproof · cited by 4
- ENNReal.exists_nat_pos_mul_gtproof · cited by 2
- Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_auxproof · cited by 1
- VitaliFamily.ae_eventually_measure_zero_of_singularproof · cited by 1
- ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self'proof · cited by 1
- MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegralproof · cited by 1
- VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrableproof · cited by 1
- ProbabilityTheory.Fernique.logRatio_mul_normThreshold_add_one_leproof · cited by 1
- MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zeroproof · cited by 1
- ENNReal.tendsto_atTop_zero_iff_lt_of_antitoneproof · cited by 1