iUnion_comm

Mathlib.Data.Set.Lattice

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

English

The union over i of the union over i' of s i i' equals the union over i' of the union over i of s i i'.

Русский

Объединение по i и i' эквивалентно объединению в обратном порядке.

LaTeX

$$$$\\bigcup_{i} \\bigcup_{i'} s(i,i') = \\bigcup_{i'} \\bigcup_{i} s(i,i')$$$$

Lean4

theorem iUnion_comm (s : ι → ι' → Set α) : ⋃ (i) (i'), s i i' = ⋃ (i') (i), s i i' :=
  iSup_comm

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

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

Разделы

Аффилиация

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