Theorems · Theorem · order theory
abs_of_nonpos
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a ≤ 0 → |a| = -a- Cited by
- 53 results in Mathlib
- Foundations
- Depth 16 from the axioms · 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
- neg_nonnegproof · cited by 60
- sup_eq_rightproof · cited by 53
Cited by53
Results whose statement or proof uses this declaration.
- abs_mulproof · cited by 98
- abs_of_negproof · cited by 39
- Int.abs_eq_natAbsproof · cited by 26
- HasSum.nat_add_negproof · cited by 10
- neg_abs_leproof · cited by 5
- Real.norm_of_nonposproof · cited by 4
- RCLike.sqrt_eq_iteproof · cited by 4
- Real.cos_absproof · cited by 4
- Monotone.tendstoLocallyUniformly_of_forall_tendstoproof · cited by 4
- Real.dist_le_of_mem_Iccproof · cited by 3
- max_sub_min_eq_abs'proof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.absproof · cited by 3