English
Given p : TwoPointing α and q : TwoPointing β, there is a TwoPointing on α × β defined by fst := (p.fst, q.fst) and snd := (p.snd, q.snd).
Русский
Пусть p — TwoPointing на α, a q — TwoPointing на β. Тогда на α × β есть TwoPointing, задаваемое fst := (p.fst, q.fst), snd := (p.snd, q.snd).
LaTeX
$$$\\text{TwoPointing.prod}(p,q)$ is a TwoPointing of $(\\alpha \\times \\beta)$ with fst := (p.fst, q.fst) and snd := (p.snd, q.snd).$$
Lean4
/-- The product of two two-pointings. -/
def prod : TwoPointing (α × β) where
fst := (p.fst, q.fst)
snd := (p.snd, q.snd)
fst_ne_snd h := p.fst_ne_snd (congr_arg Prod.fst h)
