mul_le_mul_right_iff

Mathlib.Data.ENat.Basic

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

← MathLib Explorer

English

For a ≠ 0 and a ≠ ⊤, x*a ≤ y*a iff x ≤ y.

Русский

Для a ≠ 0 и a ≠ ⊤, x·a ≤ y·a эквивалентно x ≤ y.

LaTeX

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

Lean4

@[simp]
theorem mul_le_mul_right_iff {x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a ↔ x ≤ y :=
  (ENat.mul_left_strictMono ha h_top).le_iff_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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