le_inv_of_le_inv₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

$$$0 < a \land a \le b^{-1} \Rightarrow b \le a^{-1}$$$

Lean4

theorem le_inv_of_le_inv₀ (ha : 0 < a) (h : a ≤ b⁻¹) : b ≤ a⁻¹ :=
  (le_inv_comm₀ ha <| inv_pos.1 <| ha.trans_le h).1 h

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

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

Разделы

Аффилиация

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