Theorems · Theorem · order theory
zero_le
∀ {α : Type u_1} [inst : LE α] [inst_1 : Zero α] [IsBotZeroClass α] {a : α}, 0 ≤ a- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Cited by
- 382 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 10 definitions · uses no axioms
- Assumes
- LEZeroIsBotZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsBotZeroClassstatement and proof · cited by 71
- isBot_zeroproof · cited by 2
Cited by383
Results whose statement or proof uses this declaration.
- pos_iff_ne_zeroproof · cited by 180
- nonpos_iff_eq_zeroproof · cited by 100
- zero_tsubproof · cited by 100
- eq_zero_or_posproof · cited by 54
- pos_of_gtproof · cited by 24
- MeasureTheory.lintegral_iSupproof · cited by 16
- Finset.sum_le_sum_of_subsetproof · cited by 14
- not_lt_zeroproof · cited by 11
- ContDiffWithinAt.continuousWithinAtproof · cited by 11
- MeasureTheory.MemLp.mono_exponentproof · cited by 11
- ENNReal.sum_le_tsumproof · cited by 10
- MeasureTheory.exists_measurable_le_lintegral_eqproof · cited by 8
Showing the 200 most cited of 383.