zero_def

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.zero_def

English

The zero element of languages is the empty set of words; there are no words in the zero language.

Русский

Нулевой элемент языка — это пустое множество слов; в нулевом языке нет слов.

LaTeX

$$$ (0 : Language \alpha) = \emptyset. $$$

Lean4

theorem zero_def : (0 : Language α) = (∅ : Set _) :=
  rfl

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

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

Разделы

Аффилиация

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