English
If a and b are bottoms in their respective preorderings, then their pair (a,b) is a bottom in the product preorder.
Русский
Если a и b являются нижними элементами в своих порядках, то пара (a,b) является нижним элементом в произведении.
LaTeX
$$$\\forall {\\alpha : Type*} {\\beta : Type*} [Preorder \\alpha] [Preorder \\beta] {a : \\alpha} {b : \\beta}, IsBot a \\rightarrow IsBot b \\rightarrow IsBot (\\fst := a, \\snd := b)$$$
Lean4
theorem prodMk (ha : IsBot a) (hb : IsBot b) : IsBot (a, b) := fun _ => ⟨ha _, hb _⟩