le_iff_le_iff_lt_iff_lt — Mathlib

English

Let α and β be linearly ordered sets. For elements a,b ∈ α and c,d ∈ β, the statement a ≤ b iff c ≤ d is equivalent to the statement 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) \iff (b < a \leftrightarrow d < c) $$$

Lean4

theorem le_iff_le_iff_lt_iff_lt {β} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
    (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
  ⟨lt_iff_lt_of_le_iff_le, fun H ↦ not_lt.symm.trans <| (not_congr H).trans <| not_lt⟩

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