Cardinality of a finset

Stream: maths

[Chris Birkbeck]

Hello, so I'm trying to prove a specific finset has a certain cardinality, and I'm not sure about the best way to do this in Lean.

My finset is:

def Square (m: ℕ): finset (ℤ × ℤ):=
((finset.Ico_ℤ (-m) (m+1)).product (finset.Ico_ℤ (-m) (m+1))).filter (λ x, max (x.1).nat_abs (x.2).nat_abs = m)

(i.e. pairs of integers where the maximum of the absolute values is exactly n). There might be a better way to define this finset, which makes it easier to prove the cardinality, but this is what I currently have.

Now, I would like to prove:

lemma Square_size (m : ℕ) (h: 1 ≤ m): finset.card (Square m)=8*m:=
begin
sorry,
end

Lean seems we know what the cardinality of finsets like range is, so maybe rewriting this set as a carefully chosen union of ranges might work, but this seems a bit annoying, so I wondered if there was a better way.

[Johan Commelin]

@Chris Birkbeck What is the maths proof? Probably you chop Square up into 8 finsets of size m. So you'll have to do that in Lean as well.

[Johan Commelin]

If you take the image of a finset under an embedding, then there must be some lemma finset.card_map that tells you that the cardinality doesn't change.

[Johan Commelin]

So then you only need to prove that your 8 finsets are covering and disjoint. Of course you don't want to check 8 * 7 pairs to be disjoint, so you can hopefully do something a bit smarter there, by defining a function that sends every element of Square to the appropriate finset.

[Chris Birkbeck]

Yeah the maths proofs I can think of chop it up into a few finsets (and possibly remove duplicates). So I guess I'll try that then :) Hopefully the disjointness can be done in a less painful way.

[Johan Commelin]

Maybe the nice proof is to do 4 finsets of size 2 * m + 1, and then remove duplicates?

[Chris Birkbeck]

Yes, thats what I was thinking, but I'm not sure about how to do the "remove duplicates " in Lean.

[Eric Rodriguez]

have we defined the bijection 0 1 2 3 4 ... → 0 1 -1 2 -2 ... etc? may be best to do range (2 * m + 1) × range (2 * m + 1) and take the image under that

[Eric Rodriguez]

oh this is only the edges... may be easiest to just do full-length verticals, and don't put the corners in the horizontal ones

[Chris Birkbeck]

Ah yes, I think I was just being silly, I think I can see how to remove the duplicates now (just dont include them !)