card_filter_fin_lt

Stream: Is there code for X?

[Joseph Hua]

Hi! I would like to prove this

lemma finset.card_filter_fin_lt {n k : ℕ} (h : k < n) :
  (finset.filter (λ (j : fin n), ↑j < k) finset.univ).card = k :=
sorry

I can imaging making finset.filter (λ (j : fin n), ↑j < k) finset.univ biject with finset.range k and then taking the cardinality using finset.card_range. Is there already something like this or a better way of doing things?

Would this be a useful result in the library?

[Yaël Dillies]

Have a look at data.fin.interval. What you want is basically docs#fin.card_Iio

[Joseph Hua]

Yaël Dillies said:

Have a look at data.fin.interval. What you want is basically docs#fin.card_Iio

ahaa thank you!

[Joseph Hua]

oh wow you made this very recently

[Yaël Dillies]

Yeah, this finite intervals refactor started in September and is still happening. I have branch#localfinorder_multiset for finite intervals of multisets.