English
The order on the dependent sum is given by: a ≤ b iff there exists i with a.1=b.1 and the second components satisfy the fibered inequality h.rec a.2 ≤ b.2.
Русский
Порядок на зависимой сумме задаётся следующим образом: a ≤ b тогда и только тогда, существует i такое, что a.1=b.1 и вторые компоненты удовлетворяют неравенству в волокне: h.rec a.2 ≤ b.2.
LaTeX
$$$a \\le b \\iff \\exists h : a.1 = b.1, h.rec(a.2) \\le b.2.$$$
Lean4
theorem le_def [∀ i, LE (α 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 LE.fiber _ _ _ h
