singleton_diffs_singleton

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.singleton_diffs_singleton

English

The diffs between two singleton sets {a} and {b} is the singleton {a \\ b}: ({a} \\ {b}) = {a \\ b}.

Русский

Разности между дважды одиночными множествами {a} и {b} равны одиночке {a \\ b}.

LaTeX

$$$ ({a}) \\ ({b}) = { a \\ b } $$$

Lean4

theorem singleton_diffs_singleton : ({ a } \\ { b } : Finset α) = {a \ b} :=
  image₂_singleton

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

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

Разделы

Аффилиация

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