Theorems · Theorem · order theory
sub_one_lt
∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] [ZeroLEOneClass R] [NeZero 1] [AddLeftStrictMono R] (a : R),
a - 1 < a- Cited by
- 8 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- LinearOrderstatement and proof · cited by 8,572
- Ringstatement and proof · cited by 7,463
- ZeroLEOneClassstatement and proof · cited by 304
- AddLeftStrictMonostatement and proof · cited by 203
- lt_add_oneproof · cited by 105
- sub_lt_iff_lt_addproof · cited by 39
Cited by8
Results whose statement or proof uses this declaration.
- deriv_zpowproof · cited by 4
- ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTopproof · cited by 3
- Real.log_le_rpow_divproof · cited by 2
- EReal.continuousAt_add_top_coeproof · cited by 2
- IsFiltration.mk_intproof · cited by 2
- LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable'proof · cited by 2
- Hyperreal.not_infinite_realproof · cited by 1
- tendsto_ceil_atBotproof · cited by 0