instSupSet

Mathlib.Order.SetNotation

URI: https://scilib.ai/kg/mathlib#Set.instSupSet

English

SupSet (Set α) assigns to each S a set consisting of elements that lie in some member of S.

Русский

SupSet (Set α) задаёт множество элементов, которые лежат в хотя бы одном множестве из S.

LaTeX

$$$\mathrm{SupSet}\ (\mathrm{Set}\ α) = { a \mid \exists t \in S, a \in t }$$$

Lean4

instance : SupSet (Set α) :=
  ⟨fun s => {a | ∃ t ∈ s, a ∈ t}⟩

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

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

Разделы

Аффилиация

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