iUnion_smul_right_image

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

The union over a in t of the image of s under right action by a equals s • t.

Русский

Объединение по a∈t образа множества s при правом действии на a даёт s • t.

LaTeX

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

Lean4

@[to_additive]
theorem iUnion_smul_right_image : ⋃ a ∈ t, (· • a) '' s = s • t :=
  iUnion_image_right _

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

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

Разделы

Аффилиация

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