instHasCompl

Mathlib.ModelTheory.Definability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.DefinableSet.instHasCompl

English

The complement of a definable set is again definable.

Русский

Дополнение определяемого множества снова является определяемым.

LaTeX

$$$$ ((s^c : L.DefinableSet A α) : Set(α \\to M)) = (s : Set(α \\to M))^c. $$$$

Lean4

instance instHasCompl : HasCompl (L.DefinableSet A α) :=
  ⟨fun s => ⟨sᶜ, s.2.compl⟩⟩

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

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

Разделы

Аффилиация

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