isGLB_inf_id

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.isGLB_inf_id

English

IsGLB s.toSet (s.inf id); i.e., the infimum over a set equals the glb with the identity map.

Русский

IsGLB s.toSet (s.inf id); то есть инфимума над множеством равна glo над единичной картой.

LaTeX

$$$ IsGLB s.toSet (s.inf id) $$$

Lean4

theorem isGLB_inf_id {s : Finset α} : IsGLB s (s.inf id) := by simpa using isGLB_inf (f := id)

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

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

Разделы

Аффилиация

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