Mathlib Map

Theorems · Theorem · order theory

le_total_of_codirected

∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α},
  r ≤ v₁ → r ≤ v₂ → v₁ ≤ v₂ ∨ v₂ ≤ v₁
Defined in
Mathlib.Order.SuccPred.Archimedean
Cited by
1 results in Mathlib
Foundations
Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PreorderSuccOrderIsSuccArchimedean
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

lt_or_le_of_codirected · cited by 0lt_or_le_of_codirectedPreorder · cited by 7952PreorderNat.iterate · cited by 740Nat.iterateOrder.succ · cited by 633Order.succSuccOrder · cited by 574SuccOrderIsSuccArchimedean · cited by 88IsSuccArchimedeanFunction.iterate_add · cited by 11Function.iterate_addOrder.le_succ_iterate · cited by 5Order.le_succ_iterateLE.le.exists_succ_iterate · cited by 4le.exists_succ_iteratele_total_of_codirectedCITED BYCITES

Cites8

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.