inf_id_set_eq_sInter

Mathlib.Data.Finset.Lattice.Fold

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

English

For a Finset of sets s, the infimum of the identity function equals the intersection (sInter) of the elements of s.

Русский

Для множества конечных множеств s, инфимум от id равен пересечению (sInter) элементов s.

LaTeX

$$$s.inf id = ⋂₀ \uparrow s$$$

Lean4

theorem inf_id_set_eq_sInter (s : Finset (Set α)) : s.inf id = ⋂₀ ↑s :=
  inf_id_eq_sInf _

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

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

Разделы

Аффилиация

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