compl — Mathlib

English

The complement of a set s is the set of elements not contained in s, within α: s^c = {a ∈ α | a ∉ s}.

Русский

Комплемент множества s — множество элементов, не входящих в s, внутри α: s^c = {a ∈ α | a ∉ s}.

LaTeX

$$$s^{c} = \{a \in \alpha \mid a \notin s\}$$$

Lean4

/-- The complement of a set `s` is the set of elements not contained in `s`.

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

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