English
Let α be a linear order. The maximum of a finite set s ⊆ α is defined as the supremum of s in the ambient order, i.e. s.max := sup s (↑).
Русский
Пусть α — линейный порядок. Максимум конечного множества s ⊆ α определяется как верхняя грань над множеством s, то есть s.max = sup s (↑).
LaTeX
$$$$ \\text{max}(s) = \\operatorname{sup}_{x\\in s} x. $$$$
Lean4
/-- 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'`. -/
protected def max (s : Finset α) : WithBot α :=
sup s (↑)
