op — Mathlib · SciLib

English

The opposite of a set s is the set of opposites of its elements.

Русский

Противоположное множество к s состоит из противоположных элементов его элементов.

LaTeX

$$$$ \\operatorname{op}(s) = \\{ x^{\\mathrm{op}} \\mid x \\in s \\} $$$$

Lean4

/-- The opposite of a set `s` is the set obtained by taking the opposite of each member of `s`. -/
protected def op (s : Set α) : Set αᵒᵖ :=
  unop ⁻¹' s

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