Theorems · Theorem · order theory
zero_lt_one
∀ {α : Type u_1} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1], 0 < 1See zero_lt_one' for a version with the type explicit.
- Defined in
- Mathlib.Algebra.Order.ZeroLEOne
- Cited by
- 598 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 27 definitions · uses no axioms
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.
- PartialOrderstatement and proof · cited by 6,410
- zero_le_oneproof · cited by 316
- ZeroLEOneClassstatement and proof · cited by 304
- LE.le.lt_of_neproof · cited by 116
Cited by600
Results whose statement or proof uses this declaration.
- Real.exp_posproof · cited by 169
- zero_lt_twoproof · cited by 124
- lt_add_oneproof · cited by 105
- one_posproof · cited by 102
- Real.log_oneproof · cited by 91
- ENNReal.rpow_oneproof · cited by 56
- Real.log_posproof · cited by 51
- Complex.exp_zeroproof · cited by 43
- Ordinal.isNormal_opowproof · cited by 37
- Real.rpow_le_rpow_of_exponent_leproof · cited by 32
- one_half_posproof · cited by 31
- Real.log_nonnegproof · cited by 28
Showing the 200 most cited of 600.