English
If each α_i is an ordered subtraction structure, then the function space (i ↦ α_i) inherits an OrderedSub structure pointwise: f ≤ g − h iff ∀ i, f(i) ≤ g(i) − h(i).
Русский
Если для каждого индекса i совокупности α_i задана упорядоченная структура с вычитанием, то множество функций i ↦ α_i обладает структурой OrderedSub по каждой координате: f ≤ g − h тогда и только если для всех i выполняется f(i) ≤ g(i) − h(i).
LaTeX
$$$ f \\le g - h \\iff \\forall i,\\ f(i) \\le g(i) - h(i) $$$
Lean4
instance orderedSub {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, Add (α i)] [∀ i, Sub (α i)]
[∀ i, OrderedSub (α i)] : OrderedSub ((i : ι) → α i) where
tsub_le_iff_right _ _ _ := ⟨fun w i ↦ tsub_le_iff_right.mp (w i), fun w i ↦ tsub_le_iff_right.mpr (w i)⟩
