diffs_empty

Mathlib.Data.Finset.Sups

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

English

For any finite s, the diffs with the empty right-hand argument yield the empty Finset: s \\ ∅ = ∅.

Русский

Для любого конечного s разности с пустым справа дают пустое множество: s \\ ∅ = ∅.

LaTeX

$$$ s \\ \\emptyset = \\emptyset $$$

Lean4

@[simp]
theorem diffs_empty : s \\ ∅ = ∅ :=
  image₂_empty_right

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

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

Разделы

Аффилиация

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