fst — Mathlib

English

If a pair (a,b) is bottom in the product preorder, then a is bottom in its coordinate.

Русский

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

LaTeX

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

Lean4

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

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