Theorems · Theorem · order theory
sub_pos_of_lt
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, b < a → 0 < a - bAlias of the reverse direction of sub_pos.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- AddGroupLTAddRightStrictMono
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 and proof · cited by 4,410
- AddRightStrictMonostatement and proof · cited by 160
- sub_posproof · cited by 147
Cited by40
Results whose statement or proof uses this declaration.
- hasFDerivAt_norm_rpowproof · cited by 5
- Cardinal.mk_Ioo_realproof · cited by 5
- strictConcaveOn_log_Ioiproof · cited by 5
- strictConvexOn_of_slope_strict_mono_adjacentproof · cited by 5
- Real.abs_log_sub_add_sum_range_leproof · cited by 4
- infEDist_thickeningproof · cited by 3
- HasDerivWithinAt.liminf_right_slope_norm_leproof · cited by 3
- convexOn_of_slope_mono_adjacentproof · cited by 3
- Hyperreal.isSt_iffproof · cited by 3
- Manifold.exists_lt_locally_constant_of_riemannianEDist_ltproof · cited by 3
- Real.binEntropy_posproof · cited by 3
- openSegment_sameproof · cited by 3