snd — Mathlib

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

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