le_of_not_le_of_le

Mathlib.Tactic.IntervalCases

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.IntervalCases.le_of_not_le_of_le

Lean4

theorem le_of_not_le_of_le {hi n lo : α} [LinearOrder α] (h1 : ¬hi ≤ n) (h2 : hi ≤ lo) : (n : α) ≤ lo :=
  le_trans (le_of_not_ge h1) h2

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

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

Разделы

Аффилиация

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