biUnion_ge

Mathlib.Data.Set.Lattice

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

English

Given a partially ordered index set, the union over all i of unions over j ≥ i equals the union over i of s(i).

Русский

Пусть индексный множественный набор упорядочен; ⋃_i ⋃_{j ≥ i} s(j) = ⋃_i s(i).

LaTeX

$$$$ \bigcup_{i} \bigcup_{j \ge i} s(j) = \bigcup_{i} s(i) $$$$

Lean4

theorem biUnion_ge : (⋃ j ≥ i, s j) = s i ∪ ⋃ j > i, s j :=
  biSup_ge_eq_sup s i

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

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

Разделы

Аффилиация

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