lt_def — Mathlib

English

For the lexicographic order on Lex, the lt_def asserts: a < b iff a.1 < b.1 or there exists h: a.1 = b.1 with h.rec a.2 < b.2.

Русский

Для лексикографического порядка на Lex утверждается: a < b тогда и только тогда, что a_1 < b_1 или существует h: a_1 = b_1 и h.rec a_2 < b_2.

LaTeX

$$$a < b \iff a_1 < b_1 \lor \exists h: a_1 = b_1,\; h.rec(a_2) < b_2$$$

Lean4

theorem lt_def [LT ι] [∀ i, LT (α i)] {a b : Σₗ i, α i} : a < b ↔ a.1 < b.1 ∨ ∃ h : a.1 = b.1, h.rec a.2 < b.2 :=
  Sigma.lex_iff

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