fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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