vsub

Mathlib.Algebra.Group.Pointwise.Set.Finite

URI: https://scilib.ai/kg/mathlib#Set.Finite.vsub

English

If s and t are finite subsets of β with a VSub operation, then s −ᵥ t is finite.

Русский

Если s и t — конечные подмножества β с операцией вычитания по подпространству, то s −ᵥ t конечное.

LaTeX

$$$$ hs.Finite \\land ht.Finite \\Rightarrow (s -\\u2223 t).Finite $$$$

Lean4

theorem vsub (hs : s.Finite) (ht : t.Finite) : Set.Finite (s -ᵥ t) :=
  hs.image2 _ ht

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

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

Разделы

Аффилиация

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