English
If each π(i) carries a preorder, then the function space ∀ i, π(i) carries a pointwise preorder.
Русский
Если для каждого i тип π(i) имеет предупорядоченность, то пространство функций ∀ i, π(i) имеет покомпонентный порядок.
LaTeX
$$$ \bigl( \forall i,\ Preorder(\pi(i)) \bigr) \Rightarrow \ Preorder(\forall i,\pi(i)) \text{ with } f \le g \iff \forall i, f(i) \le g(i) $$$
Lean4
instance preorder [∀ i, Preorder (π i)] : Preorder (∀ i, π i)
where
__ := inferInstanceAs (LE (∀ i, π i))
le_refl := fun a i ↦ le_refl (a i)
le_trans := fun _ _ _ h₁ h₂ i ↦ le_trans (h₁ i) (h₂ i)
