iUnion_prod_const

Mathlib.Data.Set.Lattice.Image

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

English

The iUnion of s_i × t equals the product of the iUnions: ⋃ i, s_i × t = (⋃ i s_i) × t.

Русский

Объединение по i (s_i × t) равно произведению объединений: (⋃ i s_i) × t.

LaTeX

$$$\bigcup_{i} (s_i \times t) = (\bigcup_{i} s_i) \times t$$$

Lean4

theorem iUnion_prod_const {s : ι → Set α} {t : Set β} : (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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