prod_iUnion₂

Mathlib.Data.Set.Lattice.Image

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

English

Distributes over a two-parameter union: (s ×⋃(i)(j) t(i,j)) equals ⋃(i)(j) s × t(i,j).

Русский

Распределение по двум векторам: s ×⋃(i)(j) t(i,j) = ⋃(i)(j) s × t(i,j).

LaTeX

$$$s \times (\bigcup_{i,j} t(i,j)) = \bigcup_{i,j} (s \times t(i,j))$$$

Lean4

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

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

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

Разделы

Аффилиация

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