lt_iff_lt_of_le_iff_le — Mathlib

English

If two elements a,b in a linearly ordered set α and c,d in a linearly ordered set β satisfy a ≤ b iff c ≤ d, then b < a iff d < c.

Русский

Если элементы a, b из линейно упорядоченного множества α и c, d из линейного упорядоченного множества β удовлетворяют условию a ≤ b тогда и только тогда c ≤ d, то b < a тогда и только тогда d < c.

LaTeX

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

Lean4

theorem lt_iff_lt_of_le_iff_le {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} (H : a ≤ b ↔ c ≤ d) :
    b < a ↔ d < c :=
  not_le.symm.trans <| (not_congr H).trans <| not_le

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