min_singleton

Mathlib.Data.Finset.Max

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

English

The minimum of a singleton Finset {a} is a.

Русский

Минимум множества {a} равен a.

LaTeX

$$$\min\{a\} = a$$$

Lean4

@[simp]
theorem min_singleton {a : α} : Finset.min { a } = (a : WithTop α) :=
  by
  rw [← insert_empty_eq]
  exact min_insert

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

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

Разделы

Аффилиация

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