Theorems · Theorem · order theory
abs_of_pos
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], 0 < a → |a| = a- Cited by
- 114 results in Mathlib
- Foundations
- Depth 17 from the axioms, rests on 91 definitions · uses propext
- Assumes
- LatticeAddGroupAddLeftMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- LT.lt.leproof · cited by 2,189
- absstatement · cited by 1,814
- Latticestatement and proof · cited by 916
- AddLeftMonostatement and proof · cited by 687
- abs_of_nonnegproof · cited by 279
Cited by114
Results whose statement or proof uses this declaration.
- Real.exp_logproof · cited by 58
- abs_posproof · cited by 45
- Real.abs_expproof · cited by 23
- Real.rpow_logbproof · cited by 15
- ContDiffBump.support_eqproof · cited by 8
- Real.abs_rpow_le_abs_rpowproof · cited by 7
- Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_posproof · cited by 6
- MeasureTheory.integral_comp_mul_left_Ioiproof · cited by 5
- Real.norm_twoproof · cited by 4
- Orientation.oangle_add_right_smul_rotation_pi_div_twoproof · cited by 4
- TFAE_exists_lt_isLittleO_powproof · cited by 4
- hasStrictDerivAt_abs_posproof · cited by 3