Mathlib Map

Theorems · Theorem · order theory

injective_toZ

∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι}, Function.Injective (toZ i0)
Defined in
Mathlib.Order.SuccPred.LinearLocallyFinite
Cited by
1 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.

toZ_inj · cited by 0toZ_injLinearOrder · cited by 8572LinearOrderSuccOrder · cited by 574SuccOrderPredOrder · cited by 334PredOrderStrictMono.injective · cited by 94StrictMono.injectiveIsSuccArchimedean · cited by 88IsSuccArchimedeantoZ · cited by 23toZtoZ_strictMono · cited by 3toZ_strictMonoinjective_toZCITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.