instSDiff

Mathlib.ModelTheory.Definability

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

English

Set-theoretic difference is definable within the DefinableSet structure.

Русский

Разность множеств понимается внутри структуры DefinableSet.

LaTeX

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

Lean4

instance instSDiff : SDiff (L.DefinableSet A α) :=
  ⟨fun s t => ⟨s \ t, s.2.sdiff t.2⟩⟩
    -- Why does it complain that `s ⇨ t` is noncomputable?

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

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

Разделы

Аффилиация

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