Theorems · Theorem · real analysis
EReal.neg_le_neg_iff
∀ {a b : EReal}, -a ≤ -b ↔ b ≤ a- Defined in
- Mathlib.Data.EReal.Operations
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ERealstatement and proof · cited by 793
- StrictAnti.le_iff_geproof · cited by 16
- EReal.neg_strictAntiproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- EReal.le_negproof · cited by 4
- EReal.neg_leproof · cited by 3
- EReal.negOrderIsoproof · cited by 2
- MeasureTheory.exists_lt_lowerSemicontinuous_integral_ltproof · cited by 2
- EReal.le_add_of_forall_gtproof · cited by 2
- EReal.antitone_div_right_of_nonposproof · cited by 1
- EReal.sub_lt_sub_of_lt_of_leproof · cited by 1
- EReal.sub_le_subproof · cited by 0
- MeasureTheory.exists_upperSemicontinuous_lt_integral_gtproof · cited by 0
- EReal.mul_le_mul_of_nonpos_rightproof · cited by 0