toLex_le_toLex' — Mathlib

English

The map sending a pair to its first component is monotone with respect to the lexicographic order.

Русский

Отображение пары в её первую компоненту монотонно относительно лексикографического порядка.

LaTeX

$$$$ \text{Monotone}(\text{fst}: \alpha \times_{\mathrm{lex}} \beta \to \alpha). $$$$

Lean4

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

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