smul_set_sUnion

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

Let a ∈ α and S ⊆ Set β. Then a • ⋃₀ S = ⋃_{s ∈ S} a • s.

Русский

Пусть a ∈ α и S ⊆ Set β. Тогда a • ⋃₀ S = ⋃_{s ∈ S} (a • s).

LaTeX

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

Lean4

@[to_additive]
theorem smul_set_sUnion (a : α) (S : Set (Set β)) : a • ⋃₀ S = ⋃ s ∈ S, a • s := by
  rw [sUnion_eq_biUnion, smul_set_iUnion₂]

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

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

Разделы

Аффилиация

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