iUnion₂_prod_const

Mathlib.Data.Set.Lattice.Image

URI: https://scilib.ai/kg/mathlib#Set.iUnion₂_prod_const

English

The two-parameter iUnion distributes with a constant second factor: ⋃ i, s_i × t_i = ⋃ i, s_i × t.

Русский

Двойное iUnion распределяется по константе второй координаты.

LaTeX

$$$\bigcup_i (s_i \times t_i) = \bigcup_i (s_i \times t)$$$

Lean4

theorem iUnion₂_prod_const {s : ∀ i, κ i → Set α} {t : Set β} : (⋃ (i) (j), s i j) ×ˢ t = ⋃ (i) (j), s i j ×ˢ t := by
  simp_rw [iUnion_prod_const]

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

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

Разделы

Аффилиация

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