lt_imp_lt_of_le_of_le

Mathlib.Order.Basic

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

← MathLib Explorer

English

If c ≤ a and b ≤ d, then a < b implies c < d.

Русский

Если c ≤ a и b ≤ d, то при a < b выполняется c < d.

LaTeX

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

Lean4

/-- monotonicity of `<` with respect to `→` -/
@[gcongr]
theorem lt_imp_lt_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a < b → c < d := fun hab ↦ (h₁.trans_lt hab).trans_le h₂

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

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

Разделы

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

Аффилиация

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