lt_rearrange

Mathlib.Tactic.LinearCombination.Lemmas

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

Lean4

theorem lt_rearrange {α : Type*} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a - b < 0) :
    a < b :=
  sub_neg.mp h

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

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

Разделы

Аффилиация

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