definable_empty

Mathlib.ModelTheory.Definability

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

English

The empty set is definable; the definability certificate can be chosen to be trivial.

Русский

Пустое множество определимо; сертификат определяемости может быть тривиальным.

LaTeX

$$$A.Definable L (\emptyset).$$$

Lean4

@[simp]
theorem definable_empty : A.Definable L (∅ : Set (α → M)) :=
  ⟨⊥, by
    ext
    simp⟩

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

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

Разделы

Аффилиация

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