min — Mathlib

English

The minimum of a Finset s is the least element of s when s is nonempty and is ⊤ otherwise.

Русский

Минимум множества s является наименьшим элементом s, если s непусто, и ⊤ иначе.

LaTeX

$$$s.min = \begin{cases} \min s & \text{если } s \neq \emptyset, \\ \top & \text{иначе.} \end{cases}$$$

Lean4

/-- Let `s` be a finset in a linear order. Then `s.min` is the minimum of `s` if `s` is not empty,
and `⊤` otherwise. It belongs to `WithTop α`. If you want to get an element of `α`, see
`s.min'`. -/
protected def min (s : Finset α) : WithTop α :=
  inf s (↑)

Похожие утверждения