toLex_lt_toLex' — Mathlib

English

A variant of the lexicographic order comparison for partial orders: x < y in Lex corresponds to x.1 ≤ y.1 and (x.1 = y.1 → x.2 < y.2).

Русский

Вариант сравнения лексикографического порядка для частичных порядков: x < y в Lex эквивалентно x1 ≤ y1 и (x1 = y1 → x2 < y2).

LaTeX

$$$$ x <_{\mathrm{lex}} y \iff x_1 \le y_1 \land (x_1 = y_1 \rightarrow x_2 < y_2). $$$$

Lean4

/-- Variant of `Prod.Lex.toLex_lt_toLex` for partial orders. -/
theorem toLex_lt_toLex' : toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2) :=
  by
  rw [toLex_lt_toLex]
  simp only [lt_iff_le_not_ge, le_antisymm_iff]
  tauto

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