English
If the neighbor sets of the constituents are finite, then the neighbor set of the box product is finite.
Русский
Если множества соседей в G и H конечно обобщены, то множество соседей в G □ H конечно.
LaTeX
$$If [Fintype (G.neighborSet x_1)] and [Fintype (H.neighborSet x_2)], then [Fintype ((G □ H).neighborSet x)].$$
Lean4
instance boxProdFintypeNeighborSet (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] :
Fintype ((G □ H).neighborSet x) :=
Fintype.ofEquiv
((G.neighborFinset x.1 ×ˢ { x.2 }).disjUnion ({ x.1 } ×ˢ H.neighborFinset x.2) <|
Finset.disjoint_product.mpr <| Or.inl <| neighborFinset_disjoint_singleton _ _)
((Equiv.refl _).subtypeEquiv fun y =>
by
simp_rw [Finset.mem_disjUnion, Finset.mem_product, Finset.mem_singleton, mem_neighborFinset, mem_neighborSet,
Equiv.refl_apply, boxProd_adj]
simp only [eq_comm, and_comm])
