snd — Mathlib

English

If a pair x = (a,b) is top in the product preorder, then b is top in the second coordinate.

Русский

Если пара x = (a,b) является верхним элементом произведения, то b — верхний элемент во второй координате.

LaTeX

$$$\\forall {\\alpha : Type*} {\\beta : Type*} [Preorder \\alpha] [Preorder \\beta] {x : \\Prod \\alpha \\beta}, IsTop x \\rightarrow IsTop x.2$$$

Lean4

theorem snd (hx : IsTop x) : IsTop x.2 := fun c => (hx (x.1, c)).2

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