English
Let a = (i, x) and b = (j, y) be elements of the dependent sum Σ i, α(i). Then a < b holds exactly when there exists an equality h: a.1 = b.1 such that transporting a.2 along h yields a.2 < b.2 in α(a.1).
Русский
Пусть a = (i, x) и b = (j, y) — элементы зависимого суммирования Σ i, α(i). Тогда a < b эквивалентно существованию равенства h: a.1 = b.1, для которого транспонированное по h x удовлетворяет x < y в α(a.1).
LaTeX
$$$a < b \;\Longleftrightarrow\; \exists h: a_1 = b_1,\; \mathrm{transport}(h)(a_2) < b_2$$$
Lean4
theorem lt_def [∀ i, LT (α i)] {a b : Σ i, α i} : a < b ↔ ∃ h : a.1 = b.1, h.rec a.2 < b.2 :=
by
constructor
· rintro ⟨i, a, b, h⟩
exact ⟨rfl, h⟩
· obtain ⟨i, a⟩ := a
obtain ⟨j, b⟩ := b
rintro ⟨rfl : i = j, h⟩
exact LT.fiber _ _ _ h
