coe_max'

Mathlib.Data.Finset.Max

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

English

The maximum of a finite nonempty set, when embedded into the ambient order, equals the ambient maximum.

Русский

Максимум конечного непустого множества, взятый в оболочке порядка, равен максимуму оболочки.

LaTeX

$$$\\uparrow(\\max' S) = \\max S$$$

Lean4

theorem coe_max' {s : Finset α} (hs : s.Nonempty) : ↑(s.max' hs) = s.max :=
  coe_sup' hs id

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

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

Разделы

Аффилиация

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