smul_set_univ_pi

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

c • univ.pi s = univ.pi (c • s)

Русский

c • univ.pi s = univ.pi (c • s)

LaTeX

$$$ c \\cdot \\mathrm{univ}.\\pi s = \\mathrm{univ}.\\pi (c \\cdot s) $$$

Lean4

@[to_additive]
theorem smul_set_univ_pi (c : M) (s : ∀ i, Set (π i)) : c • univ.pi s = univ.pi (c • s) :=
  piMap_image_univ_pi _ s

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

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

Разделы

Аффилиация

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