Theorems · Theorem · order theory
Nat.mono_cast
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α],
Monotone Nat.cast- Defined in
- Mathlib.Data.Nat.Cast.Order.Basic
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Monotonestatement · cited by 1,397
- AddLeftMonostatement and proof · cited by 687
- zero_le_oneproof · cited by 316
- AddMonoidWithOnestatement and proof · cited by 313
- ZeroLEOneClassstatement and proof · cited by 304
- Nat.cast_succproof · cited by 99
- le_add_of_nonneg_rightproof · cited by 69
- monotone_nat_of_le_succproof · cited by 45
Cited by76
Results whose statement or proof uses this declaration.
- Nat.cast_nonneg'proof · cited by 245
- tendsto_natCast_atTop_atTopproof · cited by 51
- Nat.cast_add_one_posproof · cited by 18
- Nat.strictMono_castproof · cited by 12
- Nat.cast_maxproof · cited by 10
- Function.hasTemperateGrowth_one_add_norm_sq_rpowproof · cited by 9
- Nat.cast_minproof · cited by 4
- Nat.cast_tsubproof · cited by 4
- schnirelmannDensity_setOfPred_mod_eq_oneproof · cited by 3
- Stirling.log_stirlingSeq_sdiff_leproof · cited by 3
- Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobsonproof · cited by 2
- Finset.ruzsa_covering_addproof · cited by 2