smul_set_insert

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

a · insert b s = insert (a · b) (a · s)

Русский

a · вставить b s = вставить (a · b) (a · s)

LaTeX

$$$ a \\cdot (\\mathrm{insert}\\; b\\; s) = \\mathrm{insert}\\ (a \\cdot b)\; (a \\cdot s) $$$

Lean4

@[to_additive]
theorem smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s) :=
  image_insert_eq ..

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

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

Разделы

Аффилиация

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