mul_inv_le_one_of_le₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If a ≤ b and b ≥ 0, then a b^{-1} ≤ 1.

Русский

Если a ≤ b и b ≥ 0, то a b^{-1} ≤ 1.

LaTeX

$$$a \le b \Rightarrow a \cdot b^{-1} \le 1$$$

Lean4

@[bound]
theorem mul_inv_le_one_of_le₀ [ZeroLEOneClass G₀] (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1 :=
  mul_inv_le_of_le_mul₀ hb zero_le_one <| by rwa [one_mul]

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

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

Разделы

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

Аффилиация

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