instHasCompl

Mathlib.Data.Set.Operations

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

English

The complement operation yields a function HasCompl on sets: s ↦ { x | x ∉ s }.

Русский

Операция дополнения задаёт отображение над множествами: s ↦ { x | x ∉ s }.

LaTeX

$$$s^c = \\{ x \\mid x \\notin s \\}$$$

Lean4

instance : HasCompl (Set α) :=
  ⟨fun s ↦ {x | x ∉ s}⟩

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

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

Разделы

Аффилиация

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