Theorems · Definition · order theory
List.SortedLT
{α : Type u_1} → [Preorder α] → List α → Propl.SortedLT means that the list is strictly monotonic.
- Defined in
- Mathlib.Data.List.Sort
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- StrictMonoproof · cited by 706
Cited by67
Results whose statement or proof uses this declaration.
- List.SortedLT.pairwisestatement · cited by 9
- List.SortedLT.nodupstatement and proof · cited by 5
- List.SortedLT.strictMono_getstatement · cited by 5
- List.Pairwise.sortedLTstatement · cited by 4
- Nat.bitIndices_sortedstatement and proof · cited by 3
- List.IsChain.sortedLTstatement · cited by 3
- List.SortedLT.sortedLEstatement and proof · cited by 3
- List.sortedLT_iff_pairwisestatement · cited by 3
- StrictMono.sortedLTstatement · cited by 2
- OrderEmbedding.sortedGT_listMapproof · cited by 2
- OrderEmbedding.sortedLT_listMapstatement · cited by 2
- List.SortedLE.sortedLT_of_nodupstatement · cited by 2