English
The neighbor finite set of a box product is the union of product components from the factors, suitably arranged.
Русский
С множество соседей box-продукта образуется как сочетание компонент соседей из множителей.
LaTeX
$$ (G.boxProd H).neighborFinset x = (G.neighborFinset x.fst × { x.snd }) ⊎ ( { x.fst } × H.neighborFinset x.snd )$$
Lean4
theorem neighborFinset_boxProd (x : α × β) [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)]
[Fintype ((G □ H).neighborSet x)] :
(G □ H).neighborFinset x =
(G.neighborFinset x.1 ×ˢ { x.2 }).disjUnion ({ x.1 } ×ˢ H.neighborFinset x.2)
(Finset.disjoint_product.mpr <| Or.inl <| neighborFinset_disjoint_singleton _ _) :=
by
-- swap out the fintype instance for the canonical one
letI : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _
convert_to (G □ H).neighborFinset x = _ using 2
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val
