English
If α,β have order structures with top, then α×β inherits a top element with le_top given coordinatewise; i.e., (x,y) ≤ top iff x ≤ top and y ≤ top.
Русский
Если у α и β есть порядок с верхней границей, то произведение α×β наследует верхнюю границу; порядок на произведении координатно задаётся: (x,y) ≤ (⊤α,⊤β) тогда и только тогда, x ≤ ⊤α и y ≤ ⊤β.
LaTeX
$$$\\top_{\\alpha\\times\\beta} \\text{ exists with } (x,y) \\le \\top_{\\alpha\\times\\beta} \\iff x \\le \\top_\\alpha \\wedge y \\le \\top_\\beta$$$
Lean4
instance instOrderTop [LE α] [LE β] [OrderTop α] [OrderTop β] : OrderTop (α × β)
where
__ := inferInstanceAs (Top (α × β))
le_top _ := ⟨le_top, le_top⟩
