instOrderBot — Mathlib

English

If α,β have order with bottom, then α×β inherits a bottom element given coordinatewise: (⊥α, ⊥β) ≤ (x,y) for all (x,y).

Русский

Если у α и β есть порядок с нижней границей, то произведение α×β наследует нижнюю границу координатно: (⊥α, ⊥β) ≤ (x,y) для всех (x,y).

LaTeX

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

Lean4

instance instOrderBot [LE α] [LE β] [OrderBot α] [OrderBot β] : OrderBot (α × β)
    where
  __ := inferInstanceAs (Bot (α × β))
  bot_le _ := ⟨bot_le, bot_le⟩

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