Theorems · Definition · order theory
List.maximum
{α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → List α → WithBot αmaximum l returns a WithBot α, the largest element of l for nonempty lists, and ⊥ for
[]
- Defined in
- Mathlib.Data.List.MinMax
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- PreorderDecidableLT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- WithBotstatement · cited by 1,498
- List.argmaxproof · cited by 15
Cited by26
Results whose statement or proof uses this declaration.
- List.maximum_of_length_posproof · cited by 7
- List.maximum_consstatement and proof · cited by 6
- List.le_maximum_of_mem'statement · cited by 3
- List.maximum_eq_botstatement · cited by 2
- List.maximum_memstatement · cited by 2
- List.maximum_ne_bot_of_length_posstatement and proof · cited by 2
- List.coe_maximum_of_length_posstatement and proof · cited by 1
- List.maximum_concatstatement · cited by 1
- List.maximum_eq_coe_iffstatement · cited by 1
- List.maximum_le_of_forall_lestatement and proof · cited by 1
- List.maximum_of_length_pos_memproof · cited by 1
- Nat.Subtype.ofNat_surjectiveproof · cited by 1