kstar_mul_le

Mathlib.Algebra.Order.Kleene

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

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 (hb : b ≤ c) (ha : a * c ≤ c) : a∗ * b ≤ c :=
  (mul_le_mul_left' hb _).trans <| kstar_mul_le_self ha

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

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

Разделы

Аффилиация

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