Mathlib Map

Theorems · Theorem · order theory

toZ_strictMono

∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, StrictMono (toZ i0)
Defined in
Mathlib.Order.SuccPred.LinearLocallyFinite
Cited by
3 results in Mathlib
Foundations
Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrderSuccOrderIsSuccArchimedeanPredOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

toZ_le_toZ · cited by 3toZ_le_toZtoZ_lt_toZ · cited by 1toZ_lt_toZinjective_toZ · cited by 1injective_toZLinearOrder · cited by 8572LinearOrderLE.le.trans · cited by 3151le.transLT.lt.le · cited by 2189lt.leNat.iterate · cited by 740Nat.iterateStrictMono · cited by 706StrictMonoLT.lt.trans_le · cited by 678lt.trans_leOrder.succ · cited by 633Order.succSuccOrder · cited by 574SuccOrderPredOrder · cited by 334PredOrdernot_lt · cited by 306not_ltOrder.pred · cited by 273Order.predle_or_gt · cited by 269le_or_gtOrder.le_succ · cited by 96Order.le_succIsSuccArchimedean · cited by 88IsSuccArchimedeantoZ · cited by 23toZtoZ_strictMonoCITED BYCITES

Cites24

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.