Theorems · Theorem · order theory
lt_tsub_iff_right
∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α],
a < b - c ↔ a + c < bSee lt_tsub_iff_right_of_le for a weaker statement in a partial order.
- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- lt_iff_lt_of_le_iff_leproof · cited by 54
- tsub_le_iff_rightproof · cited by 49
Cited by16
Results whose statement or proof uses this declaration.
- Set.Finite.encard_lt_topproof · cited by 10
- Polynomial.coeff_mirrorproof · cited by 4
- HasFPowerSeriesWithinOnBall.changeOriginproof · cited by 3
- FormalMultilinearSeries.changeOrigin_radiusproof · cited by 3
- CompositionAsSet.lt_lengthproof · cited by 3
- HasFiniteFPowerSeriesOnBall.changeOriginproof · cited by 2
- ENat.le_sub_one_of_ltproof · cited by 2
- cyclotomic_comp_X_add_one_isEisensteinAtproof · cited by 1
- FormalMultilinearSeries.changeOrigin_evalproof · cited by 1
- Real.arctan_add_arctan_lt_pi_div_twoproof · cited by 1
- lt_tsub_commproof · cited by 1
- Behrend.threeAPFree_image_sphereproof · cited by 1