min'_eq_sorted_zero

Mathlib.Data.Finset.Sort

URI: https://scilib.ai/kg/mathlib#Finset.min'_eq_sorted_zero

← MathLib Explorer

English

The minimum of a nonempty Finset equals the first element of its sorted list.

Русский

Минимум не пустого Finset равен первому элементу отсортированного списка.

LaTeX

$$$ s.min' H = (s.sort (\\le))[0] $$$

Lean4

theorem min'_eq_sorted_zero {s : Finset α} {h : s.Nonempty} :
    s.min' h = (s.sort (· ≤ ·))[0]'(by rw [length_sort]; exact card_pos.2 h) :=
  (sorted_zero_eq_min'_aux _ _ _).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru