singleton_mul

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

The left action by a singleton is the singleton image: {a} * t = { a · x | x ∈ t }.

Русский

Левое действие единичного элемента над множеством даёт образ единичного умножения: {a} * t = { a · x | x ∈ t }.

LaTeX

$$ { a } * t = (\, a ⋅ · \,) '' t $$

Lean4

@[to_additive (attr := simp)]
theorem singleton_mul : { a } * t = (a * ·) '' t :=
  image2_singleton_left

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

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

Разделы

Аффилиация

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