singleton_diffs — Mathlib

English

The difference between a singleton {a} and a finite set t equals the image of t under the map x ↦ a \\ x: {a} \\ t = image(t, x ↦ a \\ x).

Русский

Разности множества-одиночки {a} и множества t равна образу t при отображении x ↦ a \\ x: {a} \\ t = image(t, x ↦ a \\ x).

LaTeX

$$$ (\\{a\\} \\setminus t) = t.image (\\lambda x \\mapsto a \\setminus x) $$$

Lean4

@[simp]
theorem singleton_diffs : { a } \\ t = t.image (a \ ·) :=
  image₂_singleton_left

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