inv_le_of_inv_le₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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