Theorems · Theorem · order theory

IsGLB.prod

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} {a : α} {b : β},
  s.Nonempty → t.Nonempty → IsGLB s a → IsGLB t b → IsGLB (s ×ˢ t) (a, b)

Defined in

Mathlib.Order.Bounds.Basic

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext, Quot.sound

Assumes

PreorderPreorder