Theorems · Definition · order theory

Finset.max

{α : Type u_2} → [LinearOrder α] → Finset α → WithBot α

Let s be a finset in a linear order. Then s.max is the maximum of s if s is not empty, and ⊥ otherwise. It belongs to WithBot α. If you want to get an element of α, see s.max'.

Defined in

Mathlib.Data.Finset.Max

Cited by

50 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

LinearOrder