Mathlib Map

Theorems · Theorem · order theory

toZ_le_toZ

∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i ≤ toZ i0 j ↔ i ≤ j
Defined in
Mathlib.Order.SuccPred.LinearLocallyFinite
Cited by
3 results in Mathlib
Foundations
Depth 53 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.

le_of_toZ_le · cited by 0le_of_toZ_letoZ_mono · cited by 0toZ_monotoZ_le_iff · cited by 0toZ_le_iffLinearOrder · cited by 8572LinearOrderSuccOrder · cited by 574SuccOrderPredOrder · cited by 334PredOrderStrictMono.le_iff_le · cited by 104StrictMono.le_iff_leIsSuccArchimedean · cited by 88IsSuccArchimedeantoZ · cited by 23toZtoZ_strictMono · cited by 3toZ_strictMonotoZ_le_toZCITED BYCITES

Cites7

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.