English
In the Cartesian product G □ H, the degree of the vertex (a,b) equals deg_G(a) + deg_H(b), provided the relevant neighbor sets are finite.
Русский
В декартовом произведении G □ H, степень вершины (a,b) равна deg_G(a) + deg_H(b), при условии, что множества соседей конечны.
LaTeX
$$$ (G \square H).degree x = G.degree x.1 + H.degree x.2 \quad (x = (x.1, x.2)) \quad [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] [Fintype ((G \square H).neighborSet x)].$$$
Lean4
theorem degree_boxProd (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)]
[Fintype ((G □ H).neighborSet x)] : (G □ H).degree x = G.degree x.1 + H.degree x.2 :=
by
rw [degree, degree, degree, neighborFinset_boxProd, Finset.card_disjUnion]
simp_rw [Finset.card_product, Finset.card_singleton, mul_one, one_mul]
