iUnion_mul_left_image

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

The union over a in s of the left translates of t equals the product s · t: ⋃ a∈s, (a ·) t = s · t.

Русский

Объединение по всем a ∈ s левых сдвигов t равно произведению s · t.

LaTeX

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

Lean4

@[to_additive]
theorem iUnion_mul_left_image : ⋃ a ∈ s, (a * ·) '' t = s * t :=
  iUnion_image_left _

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

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

Разделы

Аффилиация

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