instSDiff

Mathlib.Data.Set.Defs

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

English

There is a dedicated SDiff operation on Set α, defined by s SDiff t = s \ t, i.e., set difference within α.

Русский

Существует операция SDiff на Set α, определённая как s SDiff t = s \ t, то есть разность множеств внутри α.

LaTeX

$$$\forall s,t \in Set\,\alpha:\ s \setminus t \in Set\,\alpha$$$

Lean4

instance : SDiff (Set α) :=
  ⟨Set.diff⟩

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

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

Разделы

Аффилиация

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