biUnion_le

Mathlib.Data.Set.Lattice

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

English

For a Preorder α and s: α → Set α, the union over n of the unions over m ≥ n of s(m) equals the union over n of s(n).

Русский

Пусть α — предпорядок; ⋃_n ⋃_{m≥n} s(m) = ⋃_n s(n).

LaTeX

$$$$ \bigcup_{n} \bigcup_{m \ge n} s(m) = \bigcup_{n} s(n) $$$$

Lean4

theorem biUnion_le : (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i :=
  biSup_le_eq_sup s i

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

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

Разделы

Аффилиация

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