min'_le_max'

Mathlib.Data.Finset.Max

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

English

For a nonempty finite S, min' ≤ max'.

Русский

Для непустого конечного S верно: min' ≤ max'.

LaTeX

$$$$s.min'(H) \le s.max'(H).$$$$

Lean4

theorem min'_le_max' (hs : s.Nonempty) : s.min' hs ≤ s.max' hs :=
  min'_le _ _ (max'_mem _ _)

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

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

Разделы

Аффилиация

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