Theorems · Theorem · order theory
neg_nonpos
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, -a ≤ 0 ↔ 0 ≤ aAlias of Left.neg_nonpos_iff.
Uses left co(ntra)variant.
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- AddGroupLEAddLeftMono
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.
- AddGroupstatement · cited by 4,410
- AddLeftMonostatement · cited by 687
- Left.neg_nonpos_iffproof · cited by 14
Cited by31
Results whose statement or proof uses this declaration.
- abs_of_nonnegproof · cited by 279
- Real.arcsin_zeroproof · cited by 9
- neg_nonpos_of_nonnegproof · cited by 5
- neg_abs_leproof · cited by 5
- jacobiTheta₂_functional_equationproof · cited by 3
- discrim_le_zeroproof · cited by 3
- mul_nonpos_iffproof · cited by 2
- PhragmenLindelof.quadrant_IVproof · cited by 2
- Complex.hasDerivAt_Gamma_one_halfproof · cited by 2
- EisensteinSeries.summand_boundproof · cited by 2
- EisensteinSeries.summand_bound_of_mem_verticalStripproof · cited by 2
- intervalIntegral.integral_pos_iff_support_of_nonneg_ae'proof · cited by 2