iUnion_union

Mathlib.Data.Set.Lattice

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

English

The union over i of t_i, with a fixed set s, satisfies (⋃ i t_i) ∪ s = ⋃ i (t_i ∪ s).

Русский

Объединение по i наборов t_i, объединенное с фиксированным s, равно ⋃_i (t_i ∪ s).

LaTeX

$$$$ \\left( \\bigcup_{i} t_i \\right) \\cup s = \\bigcup_{i} (t_i \\cup s) $$$$

Lean4

theorem iUnion_union [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
  iSup_sup

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

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

Разделы

Аффилиация

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