isLeast_min'

Mathlib.Data.Finset.Max

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

English

The minimum' is the least element of the set ↑s.

Русский

Минимальный элемент min' является наименьшим элементом множества ↑s.

LaTeX

$$$$IsLeast(\uparrow s)\,(s.min'(H)).$$$$

Lean4

theorem isLeast_min' : IsLeast (↑s) (s.min' H) :=
  ⟨min'_mem _ _, min'_le _⟩

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

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

Разделы

Аффилиация

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