unop

Mathlib.Data.Set.Opposite

URI: https://scilib.ai/kg/mathlib#Set.unop

English

The unop of a set of opposites is the set obtained by unop-ing each member.

Русский

Обратное множества противоположных элементов — это множество их выведения.

LaTeX

$$$$ \\operatorname{unop}(s) = \\operatorname{op}^{-1}(s) $$$$

Lean4

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

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

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

Разделы

Аффилиация

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