coe_snd — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{snd} = \\pi_2$$$

Lean4

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

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