English
If each α(i) carries a preorder, then the dependent sum Σ i, α(i) inherits a natural fiberwise preorder: (i,a) ≤ (j,b) holds only when i = j and a ≤ b in α(i); reflexivity and transitivity follow from the fiberwise Preorder, and the strict order is characterized by the standard lexicographic fiber condition.
Русский
Если для каждого i множество α(i) упорядочено дуальным образом, то зависимое суммирование Σ i, α(i) получает естественный порядок, сравнивая сначала по индексу, а затем по элементам в соответствующей области α(i).
LaTeX
$$$\forall (a,b) \in \Sigma i, α(i):\; a \le b \iff a_1 = b_1 \wedge a_2 \le b_2$ (в соответствующей fibers-структуре).$$
Lean4
protected instance preorder [∀ i, Preorder (α i)] : Preorder (Σ i, α i) :=
{ le_refl := fun ⟨i, a⟩ => Sigma.LE.fiber i a a le_rfl,
le_trans := by
rintro _ _ _ ⟨i, a, b, hab⟩ ⟨_, _, c, hbc⟩
exact LE.fiber i a c (hab.trans hbc),
lt_iff_le_not_ge := fun _ _ => by
constructor
· rintro ⟨i, a, b, hab⟩
rwa [mk_le_mk_iff, mk_le_mk_iff, ← lt_iff_le_not_ge]
· rintro ⟨⟨i, a, b, hab⟩, h⟩
rw [mk_le_mk_iff] at h
exact mk_lt_mk_iff.2 (hab.lt_of_not_ge h) }
