sUnion_smul

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

The union over a set of sets S smul t equals the union over s ∈ S of s smul t: ⋃₀ S • t = ⋃ s ∈ S, s • t.

Русский

Объединение множества S по smul с t равно объединению s smul t по всем s∈S.

LaTeX

$$$$ \bigcup_0 S \cdot t = \bigcup_{s \in S} (s \cdot t) $$$$

Lean4

@[to_additive]
theorem sUnion_smul (S : Set (Set α)) (t : Set β) : ⋃₀ S • t = ⋃ s ∈ S, s • t :=
  image2_sUnion_left ..

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

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

Разделы

Аффилиация

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