vsub_singleton

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

For any s and b, s −ᵥ {b} equals the image of s under the map x ↦ x −ᵥ b.

Русский

Для любого множества s и элемента b множество s −ᵥ {b} равно образу s под отображением x ↦ x −ᵥ b.

LaTeX

$$$ s -ᵥ \{ b \} = \{ x -ᵥ b \mid x ∈ s \} $$$

Lean4

@[simp low + 1]
theorem vsub_singleton (s : Set β) (b : β) : s -ᵥ { b } = (· -ᵥ b) '' s :=
  image2_singleton_right

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

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

Разделы

Аффилиация

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