iUnion_disjointed

Mathlib.Order.Disjointed

URI: https://scilib.ai/kg/mathlib#iUnion_disjointed

English

The union over i of disjointed f i equals the union over i of f i.

Русский

Объединение по i дисjointed f i равно объединению по i f i.

LaTeX

$$$\bigcup_i \operatorname{disjointed} f i = \bigcup_i f i$$$

Lean4

theorem iUnion_disjointed [PartialOrder ι] [LocallyFiniteOrderBot ι] {f : ι → Set α} : ⋃ i, disjointed f i = ⋃ i, f i :=
  iSup_disjointed f

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

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

Разделы

Аффилиация

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