Theorems · Theorem · order theory
sub_lt_comm
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, a - b < c ↔ a - c < b- Cited by
- 15 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- AddLeftStrictMonostatement and proof · cited by 203
- sub_lt_iff_lt_addproof · cited by 39
- sub_lt_iff_lt_add'proof · cited by 30
Cited by15
Results whose statement or proof uses this declaration.
- Int.fract_lt_oneproof · cited by 20
- Real.ball_eq_Iooproof · cited by 11
- nhds_basis_Ioo_posproof · cited by 4
- Real.binEntropy_lt_log_twoproof · cited by 2
- strictConvexOn_rpowproof · cited by 2
- Set.preimage_const_sub_Iioproof · cited by 2
- LinearOrderedField.cutMap_addproof · cited by 1
- Complex.stolzCone_subset_stolzSet_auxproof · cited by 1
- Archimedean.ratLt_addproof · cited by 1
- sub_lt_of_abs_sub_lt_leftproof · cited by 1
- Int.ceil_div_ceil_inv_sub_oneproof · cited by 1
- Real.pi_lt_sqrtTwoAddSeriesproof · cited by 1