Theorems · Theorem · order theory
sub_lt_self
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, 0 < b → a - b < aAlias of the reverse direction of sub_lt_self_iff.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
- Assumes
- AddGroupLTAddLeftStrictMono
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
- AddLeftStrictMonostatement and proof · cited by 203
- sub_lt_self_iffproof · cited by 8
Cited by12
Results whose statement or proof uses this declaration.
- Real.binEntropy_posproof · cited by 3
- MeasureTheory.hahn_decompositionproof · cited by 2
- closure_ordConnected_inter_ratproof · cited by 1
- ContinuousMap.sublattice_closure_eq_topproof · cited by 1
- Liouville.exists_pos_real_of_irrational_rootproof · cited by 1
- UniformConvexOn.strictConvexOnproof · cited by 1
- Int.fract_negproof · cited by 0
- ProbabilityTheory.geometricPMFRealSumproof · cited by 0
- Real.cauSeq_convergesproof · cited by 0
- Real.ball_eq_openSegmentproof · cited by 0
- IsLUB.exists_between_sub_selfproof · cited by 0
- IsLUB.exists_between_sub_self'proof · cited by 0