Theorems · Definition · order theory
List.SortedGT
{α : Type u_1} → [Preorder α] → List α → Propl.SortedGT means that the list is strictly antitonic.
- Defined in
- Mathlib.Data.List.Sort
- Cited by
- 54 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
- StrictAntiproof · cited by 204
Cited by54
Results whose statement or proof uses this declaration.
- List.SortedGT.strictAnti_getstatement · cited by 5
- List.sortedGT_iff_isChainstatement · cited by 3
- List.sortedGT_iff_pairwisestatement · cited by 3
- List.SortedGT.sortedGEstatement and proof · cited by 3
- List.SortedGT.pairwisestatement · cited by 3
- List.sortedGT_iff_getElem_gt_getElem_of_ltstatement and proof · cited by 2
- List.sortedGT_iff_strictAnti_getstatement · cited by 2
- List.sortedGT_map_ofDualstatement · cited by 2
- List.sortedGT_map_toDualstatement · cited by 2
- List.sortedGT_ofFn_iffstatement · cited by 2
- List.sortedGT_reversestatement · cited by 2
- List.sortedLT_map_ofDualstatement · cited by 2