isGreatest_max'

Mathlib.Data.Finset.Max

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

English

The maximum of S is the greatest element of the set ↑S.

Русский

Максимум множества S является наибольшим элементом множества ↑S.

LaTeX

$$$$IsGreatest(\uparrow s)(s.max' (H)).$$$$

Lean4

theorem isGreatest_max' : IsGreatest (↑s) (s.max' H) :=
  ⟨max'_mem _ _, le_max' _⟩

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

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

Разделы

Аффилиация

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