English
If α and β are ordered subtraction structures, then their Cartesian product α × β is endowed with a natural OrderedSub structure defined coordinatewise: (a,b) ≤ (a',b') − (c,d) holds iff a ≤ a' − c and b ≤ b' − d.
Русский
Если α и β — упорядоченные структуры с вычитанием, то их декартово произведение α × β наделяется естественной структурой OrderedSub коорддинатно: (a,b) ≤ (a',b') − (c,d) эквивалентно a ≤ a' − c и b ≤ b' − d.
LaTeX
$$$ (a,b) \\le (a',b') - (c,d) \\iff (a \\le a' - c) \\land (b \\le b' - d) $$$
Lean4
instance orderedSub [Preorder α] [Add α] [Sub α] [OrderedSub α] [Sub β] [Preorder β] [Add β] [OrderedSub β] :
OrderedSub (α × β) where
tsub_le_iff_right _ _
_ :=
⟨fun w ↦ ⟨tsub_le_iff_right.mp w.1, tsub_le_iff_right.mp w.2⟩, fun w ↦
⟨tsub_le_iff_right.mpr w.1, tsub_le_iff_right.mpr w.2⟩⟩
