range_smul

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

range (i ↦ a • f i) = a • range f

Русский

range (i ↦ a • f i) = a • range f

LaTeX

$$$ \\mathrm{range}\\, (\\lambda i. a \\cdot f(i)) = a \\cdot \\mathrm{range}\\, f $$$

Lean4

@[to_additive]
theorem range_smul [SMul α β] {ι : Sort*} (a : α) (f : ι → β) : range (fun i ↦ a • f i) = a • range f :=
  (smul_set_range ..).symm

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

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

Разделы

Аффилиация

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