le_kstar

Mathlib.Algebra.Order.Kleene

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

English

For any a in Kleene algebra, a ≤ a*.

Русский

Для любого элемента a в Kleene алгебре выполняется a ≤ a*.

LaTeX

$$$\forall a \in \alpha,\ a \le a^*$$

Lean4

@[simp]
theorem le_kstar : a ≤ a∗ :=
  le_trans (le_mul_of_one_le_left' one_le_kstar) kstar_mul_le_kstar

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

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

Разделы

Аффилиация

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