singleton_mul_singleton

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

A singleton times a set equals the image of the set under the singleton-multiplied map: {a} * t = {a · x | x ∈ t}.

Русский

Единичное умножение на множество равно образу множества под отображением x ↦ a · x.

LaTeX

$$ { a } * t = (fun x => a * x) '' t$$

Lean4

@[to_additive]
theorem singleton_mul_singleton : ({ a } : Set α) * { b } = {a * b} :=
  image2_singleton

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

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

Разделы

Аффилиация

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