inv_anti₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr, bound]
theorem inv_anti₀ (hb : 0 < b) (hba : b ≤ a) : a⁻¹ ≤ b⁻¹ :=
  (inv_le_inv₀ (hb.trans_le hba) hb).2 hba

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

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

Разделы

Аффилиация

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