coe_fst — Mathlib

English

The first-coordinate projection from a product lattice is a lattice homomorphism; its underlying function is the standard projection onto the first factor.

Русский

Проекция по первой координате из произведения решеток является гомоморфизмом решетки; базовая функция равна стандартной проекции на первую компоненту.

LaTeX

$$$\\operatorname{fst} = \\pi_1$$$

Lean4

@[simp, norm_cast]
theorem coe_fst : ⇑(fst (α := α) (β := β)) = Prod.fst :=
  rfl

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