add_self

Mathlib.Computability.Language

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

English

Adding a language to itself yields the language itself.

Русский

Сложение языка само с собой дает тот же язык.

LaTeX

$$$ \forall l: Language \alpha,\; l + l = l $$$

Lean4

@[simp]
theorem add_self (l : Language α) : l + l = l :=
  sup_idem _

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

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

Разделы

Аффилиация

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