lt_zero_of_zero_gt

Mathlib.Tactic.Linarith.Lemmas

URI: https://scilib.ai/kg/mathlib#lt_zero_of_zero_gt

Lean4

@[deprecated GT.gt.lt (since := "2025-06-16")]
theorem lt_zero_of_zero_gt {α : Type*} [Zero α] [LT α] {a : α} (h : 0 > a) : a < 0 :=
  h

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

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

Разделы

Аффилиация

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