one_def

Mathlib.Computability.Language

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

English

The one-element language consists of exactly the empty word; it contains only the empty string as a word.

Русский

Единичный язык состоит ровно из пустого слова; он содержит только пустую строку.

LaTeX

$$$ (1 : Language \alpha) = \{\\[\\]\\}. $$$

Lean4

theorem one_def : (1 : Language α) = ({[]} : Set (List α)) :=
  rfl

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

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

Разделы

Аффилиация

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