instNonempty

Mathlib.ModelTheory.Types

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.CompleteType.instNonempty

English

There exists a nonempty complete type over the empty theory for the given α.

Русский

Для данного α существует непустой полный тип над пустой теорией.

LaTeX

$$$Nonempty(CompleteType (\\empty : L.Theory) α)$$$

Lean4

instance instNonempty : Nonempty (CompleteType (∅ : L.Theory) α) :=
  nonempty_iff.2 (isSatisfiable_empty L)

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

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

Разделы

Аффилиация

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