le_imp_le_of_lt_imp_lt

Mathlib.Order.Defs.LinearOrder

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

← MathLib Explorer

English

If H: d < c → b < a and h: a ≤ b, then c ≤ d.

Русский

Если H: d < c → b < a и h: a ≤ b, то c ≤ d.

LaTeX

$$$ (d < c \rightarrow b < a) \\rightarrow (a \le b) \\rightarrow c \le d $$$

Lean4

theorem le_imp_le_of_lt_imp_lt {α β} [Preorder α] [LinearOrder β] {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) :
    c ≤ d :=
  le_of_not_gt fun h' => not_le_of_gt (H h') h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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