le_inv_mul_iff₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#le_inv_mul_iff₀

← MathLib Explorer

English

For hc > 0, a ≤ c⁻¹·b iff c·a ≤ b.

Русский

При hc > 0, a ≤ c⁻¹·b эквивалентно c·a ≤ b.

LaTeX

$$$\forall a,b,c\; (0 < c) \Rightarrow (a \le c^{-1} \cdot b \iff c \cdot a \le b)$$$

Lean4

/-- See `le_inv_mul_iff₀'` for a version with multiplication on the other side. -/
theorem le_inv_mul_iff₀ (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b := by
  rw [← mul_le_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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

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

Разделы

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

Аффилиация

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