vadd_set_vsub_vadd_set

Mathlib.Algebra.AddTorsor.Basic

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

English

For any v ∈ G and sets s, t ⊆ P, (v +ᵥ s) −ᵥ (v +ᵥ t) = s −ᵥ t.

Русский

Для любого v ∈ G и подмножеств s, t ⊆ P выполняется (v +ᵥ s) −ᵥ (v +ᵥ t) = s −ᵥ t.

LaTeX

$$$ (v +_{\!v} S) -_{\!v} (v +_{\!v} T) = S -_{\!v} T $$$

Lean4

@[simp]
theorem vadd_set_vsub_vadd_set (v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t := by ext;
  simp [mem_vsub, mem_vadd_set]

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

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

Разделы

Аффилиация

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