le_def — Mathlib

English

For the lexicographic order on the sigma-type Lex, we have le_def: a ≤ b iff a.1 < b.1 or there exists h: a.1 = b.1 such that h.rec a.2 ≤ b.2.

Русский

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

LaTeX

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

Lean4

theorem le_def [LT ι] [∀ i, LE (α 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

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