iUnion_smul

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

The union of quotients by i, s i, with a fixed t, equals the quotient of the union: (⋃ i, s i) • t = ⋃ i, s i • t.

Русский

Объединение smul: (⋃ i, s_i) • t = ⋃ i, (s_i • t).

LaTeX

$$$$ (\bigcup_i s_i) \cdot t = \bigcup_i (s_i \cdot t) $$$$

Lean4

@[to_additive]
theorem iUnion_smul (s : ι → Set α) (t : Set β) : (⋃ i, s i) • t = ⋃ i, s i • t :=
  image2_iUnion_left ..

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

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

Разделы

Аффилиация

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