lt_iff' — Mathlib

English

A variant of the lexicographic order inequality for partial orders: x < y iff x ≤ y and not y ≤ x, with the lexicographic decomposition.

Русский

Вариант неравенства для частичных порядков: x < y тогда, когда x ≤ y и не y ≤ x, с лексикографическим разложением.

LaTeX

$$$$ x < y \iff (x \le y) \land \lnot (y \le x). $$$$

Lean4

/-- Variant of `Prod.Lex.lt_iff` for partial orders. -/
theorem lt_iff' {x y : α ×ₗ β} :
    x < y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 < (ofLex y).2) :=
  toLex_lt_toLex'

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