iUnion

Mathlib.Order.SetNotation

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

English

iUnion takes the union over a family indexed by i, i.e., the supremum of sets s(i) over i.

Русский

iUnion берет объединение по индексовой семье i, то есть вершину i-представления множеств s(i).

LaTeX

$$$\mathrm{iUnion}\ (s) = iSup\, s$$$

Lean4

/-- Indexed union of a family of sets -/
def iUnion (s : ι → Set α) : Set α :=
  iSup s

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

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

Разделы

Аффилиация

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