biUnion_smul_finset

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.biUnion_smul_finset

English

Let s ⊆ α and t ⊆ β be finite. Then ⋃_{a ∈ s} (a • t) = s • t.

Русский

Пусть s ⊆ α и t ⊆ β конечны. Тогда ⋃_{a ∈ s} (a • t) = s • t.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem biUnion_smul_finset (s : Finset α) (t : Finset β) : s.biUnion (· • t) = s • t :=
  biUnion_image_left

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

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

Разделы

Аффилиация

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