Theorems · Theorem · order theory
eq_zero_or_pos
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α] (a : α), a = 0 ∨ 0 < a- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Cited by
- 54 results in Mathlib
- Foundations
- Depth 15 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.
- PartialOrderstatement and proof · cited by 6,410
- zero_leproof · cited by 382
- IsBotZeroClassstatement and proof · cited by 71
- LE.le.eq_or_lt'proof · cited by 27
Cited by54
Results whose statement or proof uses this declaration.
- Derivation.leibniz_powproof · cited by 10
- Ordinal.opow_addproof · cited by 9
- ENNReal.sub_mulproof · cited by 8
- NNReal.inner_le_Lp_mul_Lqproof · cited by 5
- Rat.floor_intCast_div_natCastproof · cited by 5
- CFC.nnrpow_nnrpowproof · cited by 5
- egauge_ball_le_of_one_lt_normproof · cited by 4
- Ordinal.opow_mulproof · cited by 4
- Ordinal.invVeblen₁_veblenproof · cited by 4
- HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principalproof · cited by 3
- ENNReal.le_of_forall_pos_nnreal_ltproof · cited by 3
- HolderOnWith.hausdorffMeasure_image_leproof · cited by 2