mul_iUnion

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

For sets s and a family t_i, the product distributes over a union: s * ⋃ i, t_i = ⋃ i, s * t_i.

Русский

Произведение по отношению к объединению: s * ⋃ i, t_i = ⋃ i, s * t_i.

LaTeX

$$$s * \\bigcup_i t_i = \\bigcup_i (s * t_i)$$$

Lean4

@[to_additive]
theorem mul_iUnion (s : Set α) (t : ι → Set α) : (s * ⋃ i, t i) = ⋃ i, s * t i :=
  image2_iUnion_right ..

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

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

Разделы

Аффилиация

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