Theorems · Theorem · order theory
sub_pos
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, 0 < a - b ↔ b < a- Cited by
- 147 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 65 definitions · uses propext
- Assumes
- AddGroupLTAddRightStrictMono
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
- zero_addproof · cited by 2,366
- sub_eq_add_negproof · cited by 1,023
- AddRightStrictMonostatement and proof · cited by 160
- neg_add_cancel_rightproof · cited by 75
- add_lt_add_iff_rightproof · cited by 42
Cited by147
Results whose statement or proof uses this declaration.
- sub_pos_of_ltproof · cited by 40
- Real.sin_pos_of_pos_of_lt_piproof · cited by 11
- CauSeq.le_of_existsproof · cited by 9
- Real.smoothTransition.pos_denomproof · cited by 8
- Real.holderConjugate_iffproof · cited by 6
- Sbtw.angle₁₂₃_eq_piproof · cited by 6
- EuclideanGeometry.angle_eq_pi_iff_sbtwproof · cited by 6
- hasFDerivAt_norm_rpowproof · cited by 5
- openSegment_eq_imageproof · cited by 5
- strictConvexOn_of_slope_strict_mono_adjacentproof · cited by 5
- CauSeq.const_ltproof · cited by 5
- nhds_eq_iInf_abs_subproof · cited by 5