biUnion_univ

Mathlib.Data.Set.Lattice

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

English

The union over x ∈ univ of s(x) equals the union over x of s(x).

Русский

Объединение по x ∈ univ множества s(x) равно объединению по всем x.

LaTeX

$$$\\\\bigcup_{x \\in \\mathrm{univ}} s(x) = \\bigcup_{x} s(x)$$$

Lean4

theorem biUnion_univ (s : α → Set β) : ⋃ x ∈ @univ α, s x = ⋃ x, s x :=
  iSup_univ

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

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

Разделы

Аффилиация

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