le_rearrange

Mathlib.Tactic.LinearCombination.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.LinearCombination.le_rearrange

Lean4

theorem le_rearrange {α : Type*} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b ≤ 0) :
    a ≤ b :=
  sub_nonpos.mp h

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

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

Разделы

Аффилиация

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