csSup_eq_max'

Mathlib.Order.ConditionallyCompleteLattice.Finset

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

← MathLib Explorer

English

If a finite nonempty finite set of α has an infimum, that infimum belongs to the set.

Русский

Для конечного непустого множества інфинум принадлежит самому множеству.

LaTeX

$$${\text{theorem}}$$$

Lean4

theorem csSup_eq_max' {s : Finset α} (h : s.Nonempty) : sSup ↑s = s.max' h :=
  eq_of_forall_ge_iff fun _ => (csSup_le_iff s.bddAbove h.to_set).trans (s.max'_le_iff h).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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