mem_vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

An element a is in s -ᵥ t if and only if there exist b ∈ s and c ∈ t with b -ᵥ c = a.

Русский

Элемент a принадлежит s -ᵥ t тогда и только тогда существует b ∈ s и c ∈ t such that b -ᵥ c = a.

LaTeX

$$$ a \in s -ᵥ t \iff \exists b \in s, \exists c \in t, b -ᵥ c = a $$$

Lean4

theorem mem_vsub : a ∈ s -ᵥ t ↔ ∃ b ∈ s, ∃ c ∈ t, b -ᵥ c = a :=
  mem_image₂

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

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

Разделы

Аффилиация

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