Theorems · Theorem · order theory
Nat.cast_add_one_pos
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1]
(n : ℕ), 0 < ↑n + 1- Defined in
- Mathlib.Data.Nat.Cast.Order.Basic
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Nat.cast_oneproof · cited by 2,501
- AddLeftMonostatement and proof · cited by 687
- LT.lt.trans_leproof · cited by 678
- zero_lt_oneproof · cited by 598
- Nat.cast_addproof · cited by 586
- AddMonoidWithOnestatement and proof · cited by 313
- ZeroLEOneClassstatement and proof · cited by 304
- Nat.mono_castproof · cited by 76
- Monotone.impproof · cited by 3
Cited by18
Results whose statement or proof uses this declaration.
- ENNReal.rpow_natCastproof · cited by 18
- exists_nat_one_div_ltproof · cited by 7
- CircleDeg1Lift.translationNumber_le_of_le_add_intproof · cited by 4
- Stirling.log_stirlingSeq_sdiff_hasSumproof · cited by 4
- Real.abs_log_sub_add_sum_range_leproof · cited by 4
- CircleDeg1Lift.le_translationNumber_of_add_int_leproof · cited by 4
- setOfPred_liouvilleWith_subset_auxproof · cited by 2
- Metric.uniformity_basis_dist_inv_nat_succproof · cited by 2
- Real.hasSum_pow_div_log_of_abs_lt_oneproof · cited by 1
- Behrend.exists_large_sphere_auxproof · cited by 1
- Real.dimH_univ_piproof · cited by 1