Cardinality of (fin).filter

Stream: Is there code for X?

[Riccardo Brasca]

What is the best way of proving this?

import data.fintype.card

example (n : ℕ) (i : fin n) : (finset.univ.filter (λ j, i < j)).card = n - i := sorry

I've tried to play arund with data.fin.interval, but the results are not stated using filter.

[Yaël Dillies]

Hmm... that sounds like a job for me.

[Riccardo Brasca]

I thought writing directly to you :)
In any case it is surely not difficult, but I don't see a one line proof.

[Floris van Doorn]

one step should probably be docs#finset.card_sdiff. The other part probably involves some reasoning about the map fin i -> fin n.

[Floris van Doorn]

I believe there is also an off-by-1 error in the original post

[Yaël Dillies]

We can add:

lemma fin.card_Ioi (b : fin n) : (Ioi b).card = n - b := sorry

[Yaël Dillies]

It will be direct from the result about card_Ioc adn then your lemma boils down to showing finset.univ.filter (λ j, i < j) = Ioi i, which ext, simp should do.

[Yaël Dillies]

Where's fin.order_top?

[Riccardo Brasca]

Write n+1

[Riccardo Brasca]

I was fighting with the same problem

[Riccardo Brasca]

I hate that fin 0 is empty

[Yaël Dillies]

Uh, what is the instance called?

[Floris van Doorn]

from docs#fin.bounded_lattice, right?

[Yaël Dillies]

Ah yeah, of course :face_palm:

[Riccardo Brasca]

import data.fin.interval

namespace fin

open finset

lemma Ioi_eq_finset_subtype {n : ℕ} (a : fin (n + 1)) :
  Ioi a = (Ioo (a : ℕ) (n + 1)).subtype (λ x, x < n + 1) :=
by { ext, simp [is_lt] }

lemma card_Ioi (n : ℕ) (a : fin (n + 1)) : (Ioi a).card = n - a :=
begin
  rw [Ioi_eq_finset_subtype],
  simp only [and_imp, imp_self, mem_Ioo, filter_true_of_mem, nat.card_Ioo, card_subtype,
    implies_true_iff],
  have h₁ : 1 ≤ n + 1 - ↑a := by simp [nat.one_le_iff_ne_zero, is_lt],
  rw [nat.sub_eq_iff_eq_add h₁, nat.sub_add_comm (is_le a)],
end

lemma Ioi_eq_filter {n : ℕ} (a : fin (n + 1)) : Ioi a = finset.univ.filter (λ j, a < j) :=
by { ext, simp }

lemma filter_gt_card {n : ℕ} (a : fin (n + 1)) : (finset.univ.filter (λ j, a < j)).card = n - a :=
by rw [← Ioi_eq_filter, card_Ioi]

end fin

[Yaël Dillies]

Ahah! Sorry, Riccardo. #10168

[Yaël Dillies]

@Riccardo Brasca, to be sure you see that before opening a PR.

[Riccardo Brasca]

No problem!

[Yaël Dillies]

Aaaand, you have it!