lt_iff_lex_lt — Mathlib

English

In a type with a strict order, the standard list order List.lt coincides with the lexicographic order Lex (<) on lists: List.lt l l' ↔ Lex (<) l l'.

Русский

Для типа с строгим порядком обычный порядок списков List.lt совпадает с лексикографическим порядком Lex (<) на списках.

LaTeX

$$$\\forall l,l'\\: List\\,\\alpha,\\text{ если } [LT]\\alpha ,\\ l,l' :\\ List\\alpha,\\; List.lt\\ l\\ l' \\;\\iff\\; \\mathrm{List.Lex}\\ ((<))\\ l\\ l'.$$$

Lean4

theorem lt_iff_lex_lt [LT α] (l l' : List α) : List.lt l l' ↔ Lex (· < ·) l l' := by rw [List.lt]

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