Zulip Chat Archive

Stream: general

Topic: finsupps of given "cardinality"


view this post on Zulip Johan Commelin (Jun 09 2020 at 15:38):

What is the idiomatic way to complete

import data.finsupp

variables (σ : Type*) [fintype σ]

def fintype_sum_id_eq (n : ) :
  fintype {d : σ   // d.sum (λ _, id) = n} :=
set.finite.fintype $
begin
  sorry
end

view this post on Zulip Kenny Lau (Jun 09 2020 at 15:44):

I mean each component can't exceed n

view this post on Zulip Kenny Lau (Jun 09 2020 at 16:01):

import data.finsupp

open_locale classical

variables (σ : Type*) [fintype σ]

def aux (n : ) (d : {d : σ   // d.sum (λ _, id) = n}) (s : σ) : fin (n+1) :=
d.1 s, nat.lt_succ_of_le $ sorry -- motive incorrect

theorem aux_injective (n : ) : function.injective (aux σ n) :=
λ d₁ d₂ H, subtype.eq $ finsupp.ext $ λ s, by have := congr_fun H s; convert fin.veq_of_eq this -- elaboration issues

noncomputable def fintype_sum_id_eq (n : ) :
  fintype {d : σ   // d.sum (λ _, id) = n} :=
fintype.of_injective (aux σ n) (aux_injective σ n)

view this post on Zulip Kenny Lau (Jun 09 2020 at 16:01):

Lean doesn't like me

view this post on Zulip Johan Commelin (Jun 09 2020 at 16:40):

Lean also doesn't like me.

view this post on Zulip Johan Commelin (Jun 09 2020 at 16:41):

I think we are missing some "machinery/API" here. This fact is "obvious". But not to lean.

view this post on Zulip Johan Commelin (Jun 09 2020 at 17:03):

There is finsupp.lt_wf, but I don't think it is of any use here.

view this post on Zulip Johan Commelin (Jun 11 2020 at 13:49):

With #3029 it should be easy.


Last updated: May 14 2021 at 22:15 UTC