Union of family of finsets indexed by vertices

Stream: Is there code for X?

[Rida Hamadani]

Is there code for the indexed union of a family of finsets (instead of sets), which yields a finset?

I'm trying to prove that a regular graph of degree r and girth 5, will have at least 1 + r^2.
The proof is straightforward: take a vertex a, it has r vertices in its neighborhood, each of which have r - 1 other vertices in their neighborhood, all of which are distinct (otherwise we would have a triangle, contradicting girth = 5), so in total we counted 1 + r + r * (r - 1) = 1 + r^2 distinct vertices.

But when I tried to implement this proof in lean, the following code:

import Mathlib.Combinatorics.SimpleGraph.Girth
open SimpleGraph
universe u

variable {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  {r : ℕ} (hr : G.IsRegularOfDegree r) (hg : G.girth = 5)

lemma card_vertices_ge_degree_squared_plus_one : r^2 + 1 ≤ Fintype.card V := by
  have hna : ¬G.IsAcyclic := by
    rw [← girth_eq_top, hg]
    nofun
  rw [← exists_girth_eq_length] at hna
  let ⟨a, _, _, _⟩ := hna
  let s : (G.neighborFinset a ∪ (⋃ (v : G.neighborFinset a), G.neighborFinset v)).card = r^2 + 1 := by
    sorry
  sorry

Gives this error:

application type mismatch
  neighborFinset G a ∪ ⋃ v, ?m.90012 v
argument
  ⋃ v, ?m.90012 v
has type
  Set ?m.89582 : Type u
but is expected to have type
  Finset V : Type u

Is there a way to convert this set into a finset? It is a finite union of finite sets afterall.

[Matt Diamond]

docs#Finset.biUnion should work

[Matt Diamond]

Finset.biUnion (G.neighborFinset a) fun v => G.neighborFinset v

[Rida Hamadani]

That worked, thank you! :grinning_face_with_smiling_eyes:

[Matt Diamond]

no problem!

[Notification Bot]

Rida Hamadani has marked this topic as resolved.

[Yaël Dillies]

Please use docs#FInset.sup rather! Finset.biUnion will be deleted at some point in the future.

[Rida Hamadani]

Yaël Dillies said:

Please use docs#FInset.sup rather!

Doesn't this mean "the maximum of the finset", which is different from its union?

[Yaël Dillies]

If you have S : Finset (Finset α), then S.sup id is the supremum, aka union, of all s ∈ S.

[Notification Bot]

Rida Hamadani has marked this topic as unresolved.

[Rida Hamadani]

I'm trying to use #docs.Finset.sup, but it seems that I will need to:

• Define the set containing the G.neighborFinset v for each v in G.neighborFinset a as a Finset (recursively?) using docs#Finset.cons, removing duplicates if necessary.
• Find a way to talk about the cardinality of the Finset.sup. Skimming through the docs, I couldn't find an easy way to do so, ideally, it should be just the sum of the card of the Finsets, given that all these Finsets are disjoined.
• If there is a way to do that, I'll need to prove that these sets are disjoined.

Is this correct so far? Can you guide me to where I can do these steps (or any better procedures) in the docs?

[Yaël Dillies]

• No, it's already defined for you. I think the finset you want is (G.neighborFinset a).sup G.neighborFinset
• Annoyingly, docs#Finset.card_sup doesn't exist, so you will have to use docs#Finset.sup_eq_biUnion and docs#Finset.card_biUnion
• That will be fiddly because you need to use your girth hypothesis

[Rida Hamadani]

Since we are going to use docs#Finset.sup_eq_biUnion, this makes me wonder, is it okay to just define the finset to be like Matt suggested:

let s : (Finset.sup (G.neighborFinset a) fun v => G.neighborFinset v).card = r^2 + 1 := by

I couldn't get (G.neighborFinset a).sup G.neighborFinset to compile (tried many variations), and Matt's definition seems convenient for when I'll need to use docs#Finset.card_biUnion.
Also, since Finset.biUnion will get deleted at some point, does this mean that Finset.card_sup is a TODO?

[Yaël Dillies]

Sorry, I don't understand your message. What is Matt's suggestion?

[Rida Hamadani]

Matt Diamond said:

Finset.biUnion (G.neighborFinset a) fun v => G.neighborFinset v

This, but replacing Finset.biUnion by Finset.sup.

[Yaël Dillies]

Can you provide a #mwe ? Finset.sup and Finset.biUnion really are the same function, so it's strange that you can use one but not the other

[Rida Hamadani]

Sorry I think I miscommunicated, what I meant is that this:

Finset.sup (G.neighborFinset a) fun v => G.neighborFinset v

worked, but I couldn't get this

(G.neighborFinset a).sup G.neighborFinset

to work.
Here is an #mwe of the version that is not working (actually, is it an #mwe if it is not working?):

import Mathlib.Combinatorics.SimpleGraph.Girth
open SimpleGraph
universe u

variable {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  {r : ℕ} (hr : G.IsRegularOfDegree r) (hg : G.girth = 5)

lemma card_vertices_ge_degree_squared_plus_one : r^2 + 1 ≤ Fintype.card V := by
  have hna : ¬G.IsAcyclic := by
    rw [← girth_eq_top, hg]
    nofun
  rw [← exists_girth_eq_length] at hna
  let ⟨a, _, _, _⟩ := hna
  let s : (Finset.sup (G.neighborFinset a).sup G.neighborFinset Id).card = r^2 + 1 := by
    sorry
  sorry

Meanwhile, this version is working, but it doesn't use S.sup id, so I don't really understand how it is considered the "union" and not the "supremum":

import Mathlib.Combinatorics.SimpleGraph.Girth
open SimpleGraph
universe u

variable {V : Type u} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  {r : ℕ} (hr : G.IsRegularOfDegree r) (hg : G.girth = 5)

lemma card_vertices_ge_degree_squared_plus_one : r^2 + 1 ≤ Fintype.card V := by
  have hna : ¬G.IsAcyclic := by
    rw [← girth_eq_top, hg]
    nofun
  rw [← exists_girth_eq_length] at hna
  let ⟨a, _, _, _⟩ := hna
  let s : (Finset.sup (G.neighborFinset a) fun v => G.neighborFinset v).card = r^2 + 1 := by
    sorry
  sorry

[Yaël Dillies]

Ah yes of course. That's because there is an extra argument to docs#SimpleGraph.neighborFinset after the explicit (v : V)