kstar_mul_le_kstar

Mathlib.Algebra.Order.Kleene

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

English

If b ≤ c and a·c ≤ c then a*·b ≤ c.

Русский

Если b ≤ c и a·c ≤ c, то a*·b ≤ c.

LaTeX

$$$\forall a,b,c \in \alpha,\ b \le c \Rightarrow a \cdot c \le c \Rightarrow a^* \cdot b \le c$$$

Lean4

theorem kstar_mul_le_kstar : a∗ * a ≤ a∗ :=
  KleeneAlgebra.kstar_mul_le_kstar _

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

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

Разделы

Аффилиация

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