diff — Mathlib

English

The difference s \ t is the set of elements contained in s but not in t: s \ t = {a ∈ s | a ∉ t}.

Русский

Разность s \ t — множество элементов, входящих в s, но не в t: s \ t = {a ∈ s | a ∉ t}.

LaTeX

$$$s \setminus t = \{a \in s \mid a \notin t\}$$$

Lean4

/-- The difference of two sets `s` and `t` is the set of elements contained in `s` but not in `t`.

Note that you should **not** use this definition directly, but instead write `s \ t`. -/
protected def diff (s t : Set α) : Set α :=
  {a ∈ s | a ∉ t}

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