vsub_mem_vsub — Mathlib

English

Let s and t be subsets. If b ∈ s and c ∈ t, then b −ᵥ c ∈ s −ᵥ t, i.e., every difference of an element of s with an element of t lies in the set of all differences x −ᵥ y with x ∈ s and y ∈ t.

Русский

Пусть s и t — подмножества. Если b ∈ s и c ∈ t, то b −ᵥ c ∈ s −ᵥ t, то есть каждый разности элемента s и элемента t принадлежит множеству всех x −ᵥ y с x ∈ s и y ∈ t.

LaTeX

$$$ b \in s \land c \in t \Rightarrow b -ᵥ c \in s -ᵥ t $$$

Lean4

theorem vsub_mem_vsub (hb : b ∈ s) (hc : c ∈ t) : b -ᵥ c ∈ s -ᵥ t :=
  mem_image2_of_mem hb hc

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