empty_theory_categorical

Mathlib.ModelTheory.Satisfiability

URI: https://scilib.ai/kg/mathlib#Cardinal.empty_theory_categorical

English

In the empty language, the κ-categoricity of the empty theory holds for any cardinal κ.

Русский

В пустом языке теория пустоты κ-категорична при любом кардинале κ.

LaTeX

$$$\\kappa\\text{-Categorical}(T)\\quad\\text{for } T = \\text{Language.empty.Theory}.$$

Lean4

theorem empty_theory_categorical (T : Language.empty.Theory) : κ.Categorical T := fun M N hM hN => by
  rw [empty.nonempty_equiv_iff, hM, hN]

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

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

Разделы

Аффилиация

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