iUnion_op_smul_set

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

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

English

The union over a ∈ t of (op a) • s equals s * t.

Русский

Объединение по a ∈ t от (op a) · s даёт s * t.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem iUnion_op_smul_set (s t : Set α) : ⋃ a ∈ t, MulOpposite.op a • s = s * t :=
  iUnion_image_right _

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

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

Разделы

Аффилиация

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