min_of_nonempty

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.min_of_nonempty

English

If s is nonempty, there exists a with s.min = a.

Русский

Если s непусто, существует a, такое что s.min = a.

LaTeX

$$$s \neq \emptyset \Rightarrow \exists a, s.min = a$$$

Lean4

theorem min_of_nonempty {s : Finset α} (h : s.Nonempty) : ∃ a : α, s.min = a :=
  let ⟨_, h⟩ := h
  min_of_mem h

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

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

Разделы

Аффилиация

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