Product of locally finite simple graphs

Stream: Is there code for X?

[Rémi Bottinelli]

Hi,
I need to know that the product of two locally finite graphs is locally finite, as follows:

instance [Glf : locally_finite G] [Glf' : locally_finite G']: locally_finite (G □ G') := by
{
  rintro ⟨g,g'⟩,
  have : (G □ G').neighbor_set ⟨g,g'⟩ =
    ((λ x, (⟨x,g'⟩ : V × V')) '' (G.neighbor_set g)) ∪
    ((λ x', (⟨g,x'⟩ : V × V')) '' (G'.neighbor_set g')), by
  { ext ⟨x,x'⟩,
    simp only [mem_neighbor_set, box_prod_adj, mem_union_eq, set.mem_image, prod.mk.inj_iff,
               exists_eq_right_right],
    simp_rw and_comm _ (g' = x'),
    simp only [exists_eq_right_right],tauto,},
  rw this,
  apply set.finite.fintype,
  apply set.finite.union;
  apply set.finite.image;
  apply set.finite.intro,
  exact Glf g,
  exact Glf' g',
}

I couldn't fid that anywhere. Did I miss something?

[Yaël Dillies]

Everything about the box product is currently in file#combinatorics/simple_graph/prod and file#combinatorics/simple_graph/hasse, so my guess is no!

[Yaël Dillies]

You can however provide this constructively using docs#fintype.of_equiv.

[Rémi Bottinelli]

because the détour by set.finite breaks constructiv(ity|ness), I assume?

[Rémi Bottinelli]

Anyway, thanks for the confirmation, this would be a good exercise PR for me …

Actually, I don't really see where you'd use fintype_of_equiv ? Do you mean decomposing subtype $ (G □ G').neighbor_set ⟨g,g'⟩ first into a disjoint sum types, and doing what I did in set V×V' instead at the type level?