Theorems · Theorem · order theory
abs_of_nonneg
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 ≤ a → |a| = a- Cited by
- 279 results in Mathlib
- Foundations
- Depth 16 from the axioms, rests on 86 definitions · uses propext
- Assumes
- LatticeAddGroupAddLeftMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- LE.le.transproof · cited by 3,151
- absstatement · cited by 1,814
- Latticestatement and proof · cited by 916
- AddLeftMonostatement and proof · cited by 687
- sup_eq_leftproof · cited by 71
- neg_nonposproof · cited by 31
Cited by279
Results whose statement or proof uses this declaration.
- Real.norm_of_nonnegproof · cited by 135
- abs_of_posproof · cited by 114
- abs_mulproof · cited by 98
- abs_zeroproof · cited by 88
- abs_oneproof · cited by 87
- Nat.abs_castproof · cited by 36
- abs_normproof · cited by 36
- MeasureTheory.integral_eq_lintegral_of_nonneg_aeproof · cited by 31
- Int.abs_eq_natAbsproof · cited by 26
- NNReal.abs_eqproof · cited by 25
- MeasureTheory.ofReal_integral_eq_lintegral_ofRealproof · cited by 22
- Complex.norm_of_nonnegproof · cited by 20
Showing the 200 most cited of 279.