lt_imp_lt_of_le_imp_le — Mathlib

English

If a ≤ b and c ≤ d hold and d < c, then b < a; i.e., a ≤ b together with a reverse inequality on c,d implies a strong reversal of the order.

Русский

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

LaTeX

$$$ (H : a \\le b \\rightarrow c \\le d) \\land (h : d < c) \\Rightarrow b < a $$$

Lean4

theorem lt_imp_lt_of_le_imp_le {β} [LinearOrder α] [Preorder β] {a b : α} {c d : β} (H : a ≤ b → c ≤ d) (h : d < c) :
    b < a :=
  lt_of_not_ge fun h' ↦ (H h').not_gt h

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