lt_iff_lex_lt — Mathlib

English

For l,m in Profinite.NobelingProof.Products I with a LinearOrder I, l < m if and only if List.Lex(· < ·) l.val m.val.

Русский

Для элементов l,m в Profinite.NobelingProof.Products I с линейным порядком I выполняется: l < m тогда и только если List.Lex(· < ·) l.val m.val.

LaTeX

$$$$ l < m \\iff \\mathrm{List.Lex}(<)(l.Data)(m.Data). $$$$

Lean4

@[simp]
theorem lt_iff_lex_lt (l m : Products I) : l < m ↔ List.Lex (· < ·) l.val m.val := by simp

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