Theorems · Definition · order theory
List.minimum
{α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → List α → WithTop αminimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for
[]
- Defined in
- Mathlib.Data.List.MinMax
- Cited by
- 24 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
- WithTopstatement · cited by 3,754
- List.argminproof · cited by 13
Cited by25
Results whose statement or proof uses this declaration.
- List.minimum_consstatement and proof · cited by 7
- List.minimum_of_length_posproof · cited by 5
- List.minimum_eq_topstatement · cited by 4
- List.minimum_le_of_mem'statement · cited by 2
- List.minimum_ne_top_of_length_posstatement and proof · cited by 2
- List.not_lt_minimum_of_memstatement · cited by 1
- List.not_lt_minimum_of_mem'statement and proof · cited by 1
- List.coe_minimum_of_length_posstatement and proof · cited by 1
- List.minimum_concatstatement · cited by 1
- List.minimum_eq_coe_iffstatement · cited by 1
- List.minimum_memstatement · cited by 1
- List.minimum_of_length_pos_le_iffstatement · cited by 1