le_imp_le_iff_lt_imp_lt — Mathlib

English

Equivalence of two implications: a ≤ b implies c ≤ d iff d < c implies b < a, in a setting with two linear orders.

Русский

Эквивалентность двух следствий: a ≤ b ⇒ c ≤ d тогда и только тогда, что d < c ⇒ b < a.

LaTeX

$$$ a \\le b \\rightarrow c \\le d \\iff d < c \\rightarrow b < a $$$

Lean4

theorem le_imp_le_iff_lt_imp_lt {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
    a ≤ b → c ≤ d ↔ d < c → b < a :=
  ⟨lt_imp_lt_of_le_imp_le, le_imp_le_of_lt_imp_lt⟩

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