instBoundedOrder — Mathlib

English

If α and β are bounded orders, then α×β is a bounded order with top and bottom defined coordinatewise: top is (⊤α, ⊤β) and bottom is (⊥α, ⊥β).

Русский

Если α и β – ограниченные порядки, то произведение α×β является ограниченным порядком с верхней и нижней границей, заданными координатно: ⊤=(⊤α,⊤β), ⊥=(⊥α, ⊥β).

LaTeX

$$(\\top_{\\alpha\\times\\beta} = (\\top_\\alpha, \\top_\\beta)) \land (\\bot_{\\alpha\\times\\beta} = (\\bot_\\alpha, \\bot_\\beta))$$

Lean4

instance instBoundedOrder [LE α] [LE β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (α × β)
    where
  __ := inferInstanceAs (OrderTop (α × β))
  __ := inferInstanceAs (OrderBot (α × β))

Похожие утверждения