mem_vsub

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

a ∈ s -ᵥ t iff ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a

Русский

a ∈ s -ᵥ t эквивалентно существованию x ∈ s и y ∈ t such that x -ᵥ y = a

LaTeX

$$$ a \\in s -ᵥ t \\iff \\exists x \\in s, \\exists y \\in t, x -ᵥ y = a $$$

Lean4

theorem mem_vsub : a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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