mul_kstar_le

Mathlib.Algebra.Order.Kleene

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_kstar_le (hb : b ≤ c) (ha : c * a ≤ c) : b * a∗ ≤ c :=
  (mul_le_mul_right' hb _).trans <| mul_kstar_le_self ha

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

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

Разделы

Аффилиация

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