lt_iff_lt_of_le_iff_le' — Mathlib

English

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

Русский

Если a ≤ b ⇔ c ≤ d и b ≤ a ⇔ d ≤ c, тогда b < a ⇔ d < c.

LaTeX

$$$ b < a \\iff d < c \\;\\text{given } (a \\le b \\leftrightarrow c \\le d) \\text{ and } (b \\le a \\leftrightarrow d \\le c) $$$

Lean4

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

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