English
If a pair (a,b) is bottom in the product preorder, then b is bottom in its coordinate.
Русский
Если пара (a,b) является нижним элементом в произведении, то b — нижний элемент во второй координате.
LaTeX
$$$\\forall {\\alpha : Type*} {\\beta : Type*} [Preorder \\alpha] [Preorder \\beta] {x : \\Prod \\alpha \\beta}, IsBot x \\rightarrow IsBot x.2$$$
Lean4
theorem snd (hx : IsBot x) : IsBot x.2 := fun c => (hx (x.1, c)).2