singleton_vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.singleton_vsub

English

({a}) -ᵥ t = { a -ᵥ y | y ∈ t }.

Русский

({a}) -ᵥ t = { a -ᵥ y | y ∈ t }.

LaTeX

$$$ (\{ a \} : Finset \beta) -ᵥ t = t.image (\,a -ᵥ \cdot\,) $$$

Lean4

theorem singleton_vsub (a : β) : ({ a } : Finset β) -ᵥ t = t.image (a -ᵥ ·) :=
  image₂_singleton_left

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

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

Разделы

Аффилиация

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