English
A family of ordered sets indexed by α yields a pointwise preorder on the dependent finitely supported functions: f ≤ g iff for all a, f(a) ≤ g(a).
Русский
Для семейства упорядоченных по α множеств образуется поко-упорядочение по координатам: f ≤ g тогда и только если для всех a верно f(a) ≤ g(a).
LaTeX
$$$ f \le g \iff \forall a, f(a) \le g(a) $$$
Lean4
instance : Preorder (Π₀ i, α i) :=
{ (inferInstance : LE (DFinsupp α)) with
le_refl := fun _ _ ↦ le_rfl
le_trans := fun _ _ _ hfg hgh i ↦ (hfg i).trans (hgh i) }