refl

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeGrammar.Derives.refl

English

For every w, w derives w under the derivation relation.

Русский

Для любой последовательности w отношение вывода содержит w как саму себя.

LaTeX

$$$\forall w,\ g.Derives\ w\ w$$$

Lean4

@[refl]
theorem refl (w : List (Symbol T g.NT)) : g.Derives w w :=
  Relation.ReflTransGen.refl

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

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

Разделы

Аффилиация

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