singleton_vsub_singleton

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

({a}) -ᵥ ({b}) = { a -ᵥ b }.

Русский

({a}) -ᵥ ({b}) = { a -ᵥ b }.

LaTeX

$$$ (\{ a \} : Finset \beta) -ᵥ (\{ b \} : Finset \beta) = \{ a -ᵥ b \} $$$

Lean4

theorem singleton_vsub_singleton (a b : β) : ({ a } : Finset β) -ᵥ { b } = {a -ᵥ b} :=
  image₂_singleton

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

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

Разделы

Аффилиация

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