Theorems · Theorem · order theory
zero_le_one
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [ZeroLEOneClass α], 0 ≤ 1zero_le_one with the type argument implicit.
- Defined in
- Mathlib.Algebra.Order.ZeroLEOne
- Cited by
- 316 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 12 definitions · uses no axioms
- Assumes
- ZeroOneLEZeroLEOneClass
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.
- ZeroLEOneClassstatement and proof · cited by 304
- ZeroLEOneClass.zero_le_oneproof · cited by 1
Cited by316
Results whose statement or proof uses this declaration.
- zero_lt_oneproof · cited by 598
- abs_oneproof · cited by 87
- Nat.mono_castproof · cited by 76
- ENNReal.rpow_oneproof · cited by 56
- one_le_twoproof · cited by 44
- zero_le_twoproof · cited by 44
- Finset.prod_nonnegproof · cited by 39
- div_le_one_of_le₀proof · cited by 31
- pow_right_mono₀proof · cited by 19
- zero_le_one'proof · cited by 18
- orthonormal_iff_iteproof · cited by 15
- Real.toNNReal_oneproof · cited by 13
Showing the 200 most cited of 316.