vsub_mem_vsub

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

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

English

If b ∈ s and c ∈ t, then b -ᵥ c ∈ s -ᵥ t.

Русский

Если b ∈ s и c ∈ t, то b -ᵥ c ∈ s -ᵥ t.

LaTeX

$$$ b \in s \rightarrow c \in t \rightarrow b -ᵥ c \in s -ᵥ t $$$

Lean4

theorem vsub_mem_vsub : b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t :=
  mem_image₂_of_mem

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

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

Разделы

Аффилиация

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