definable_univ

Mathlib.ModelTheory.Definability

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

English

The entire domain is definable in any language with respect to any structure.

Русский

Вся область определения определима в любом языке относительно любой структуры.

LaTeX

$$$A.Definable L (\text{univ} : Set (\alpha \to M)).$$$

Lean4

@[simp]
theorem definable_univ : A.Definable L (univ : Set (α → M)) :=
  ⟨⊤, by
    ext
    simp⟩

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

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

Разделы

Аффилиация

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