diffs_singleton

Mathlib.Data.Finset.Sups

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

English

The left-hand difference with a fixed element b distributes over s: s \\ {b} equals the image of s under x \mapsto x \\ b.

Русский

Левая разность по элементу b распространяется на s: s \\ {b} = image(s, x ↦ x \\ b).

LaTeX

$$$ s \\{b\\} = s.image (\\cdot \\setminus b) $$$

Lean4

@[simp]
theorem diffs_singleton : s \\ { b } = s.image (· \ b) :=
  image₂_singleton_right

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

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

Разделы

Аффилиация

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