mul_le_mul_of_le_right

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.mul_le_mul_of_le_right

English

If x ≤ y and a ≠ 0, a ≠ ⊤, then x*a ≤ y*a.

Русский

Если x ≤ y и a ≠ 0, a ≠ ⊤, то x*a ≤ y*a.

LaTeX

$$$$\forall x,y,a \in \mathbb{N}_\infty,\ x \le y \land a \ne 0 \land a \ne \top \Rightarrow x \cdot a \le y \cdot a.$$$$

Lean4

@[gcongr]
theorem mul_le_mul_of_le_right {x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a := by
  simpa [ha, h_top]

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

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

Разделы

Аффилиация

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