union_iUnion

Mathlib.Data.Set.Lattice

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

English

If ι is nonempty, then s ∪ ⋃ i t_i = ⋃ i (s ∪ t_i).

Русский

Если ι непусто, то s ∪ ⋃_i t_i = ⋃_i (s ∪ t_i).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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