one_le_kstar

Mathlib.Algebra.Order.Kleene

URI: https://scilib.ai/kg/mathlib#one_le_kstar

English

In any Kleene algebra, 1 ≤ a* for every element a.

Русский

В любой Kleene-алгебре для любого элемента a выполняется 1 ≤ a*.

LaTeX

$$$1 \le a^{\star}$$$

Lean4

@[simp]
theorem one_le_kstar : 1 ≤ a∗ :=
  KleeneAlgebra.one_le_kstar _

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

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

Разделы

Аффилиация

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