sup_id_set_eq_sUnion

Mathlib.Data.Finset.Lattice.Fold

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

English

The supremum of the pointwise identity over a Finset of sets equals the union of those sets.

Русский

Супремум по точечному тождественному отображению над Finset множеств равен объединению этих множеств.

LaTeX

$$$s.sup id = \bigcup_{S\in s} S$$$

Lean4

theorem sup_id_set_eq_sUnion (s : Finset (Set α)) : s.sup id = ⋃₀ ↑s :=
  sup_id_eq_sSup _

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

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

Разделы

Аффилиация

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