Theorems · Theorem · number theory
lt_add_one
∀ {α : Type u_1} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1]
[AddLeftStrictMono α] (a : α), a < a + 1- Defined in
- Mathlib.Algebra.Order.Monoid.NatCast
- Cited by
- 105 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 44 definitions · uses no axioms
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.
- PartialOrderstatement and proof · cited by 6,410
- AddZeroClassstatement and proof · cited by 1,237
- zero_lt_oneproof · cited by 598
- ZeroLEOneClassstatement and proof · cited by 304
- AddLeftStrictMonostatement and proof · cited by 203
- lt_add_of_pos_rightproof · cited by 51
Cited by105
Results whose statement or proof uses this declaration.
- one_lt_twoproof · cited by 67
- Polynomial.derivative_mapproof · cited by 17
- exists_pos_mul_ltproof · cited by 13
- ContDiffOn.ftaylorSeriesWithinproof · cited by 11
- sub_one_ltproof · cited by 8
- HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOnproof · cited by 8
- Int.ceil_lt_add_oneproof · cited by 7
- Polynomial.as_sum_range_C_mul_X_powproof · cited by 6
- Ordinal.lift_cof_iSup_add_oneproof · cited by 4
- ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBotproof · cited by 4
- ContDiff.differentiable_iteratedFDerivproof · cited by 4
- Bornology.IsBounded.subset_ball_ltproof · cited by 4