Theorems · Inductive type · order theory
IsStrictTotalOrder
(α : Sort u_1) → (α → α → Prop) → Prop
IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order,
that is, Std.Trichotomous lt and IsStrictOrder X lt.
- Defined in
- Mathlib.Order.Defs.Unbundled
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by13
Results whose statement or proof uses this declaration.
- linearOrderOfSTOstatement and proof · cited by 11
- RelEmbedding.isWellOrderproof · cited by 4
- Pi.Lex.wellFoundedstatement and proof · cited by 2
- Concept.isCompl_extent_intentstatement and proof · cited by 2
- RelEmbedding.isStrictTotalOrderstatement and proof · cited by 1
- Finsupp.Lex.wellFounded_of_finitestatement and proof · cited by 1
- DFinsupp.Lex.wellFounded_of_finitestatement and proof · cited by 0
- Function.Injective.isStrictTotalOrder_onFunstatement and proof · cited by 0
- Concept.compl_extentstatement and proof · cited by 0
- Concept.compl_intentstatement and proof · cited by 0
- IsStrictTotalOrder.casesOnstatement and proof · cited by 0
- IsStrictTotalOrder.recOnstatement and proof · cited by 0