singleton_vsub_singleton — Mathlib

English

The vsub of two singleton sets is the singleton of the difference: {b} −ᵥ {c} = { b −ᵥ c }.

Русский

Разность по векторному вычитанию двух одиночных множеств даёт такое же единичное множество: {b} −ᵥ {c} = { b −ᵥ c }.

LaTeX

$$$ { b } -ᵥ { c } = \{ b -ᵥ c \} $$$

Lean4

@[simp high]
theorem singleton_vsub_singleton : ({ b } : Set β) -ᵥ { c } = {b -ᵥ c} :=
  image2_singleton

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