Zulip Chat Archive

Stream: general

Topic: finset.sum and injective maps

Johan Commelin (Jun 23 2021 at 17:57):

Random bit from LTE:

/-- The obvious embedding from `fin M` to `fin N` for `M ≤ N`. -/
private def ι {M N : } (h : M  N) : fin M  fin N := (fin.cast_le h).to_embedding

-- Should this be in mathlib?
lemma sum_eq_sum_map_ι {M N : } (h : M  N) (f : fin N  0) :
   i, f (ι h i) =  j in finset.map (ι h) finset.univ, f j :=
finset.sum_bij' (λ a _, ι h a) (λ a ha, by {rw mem_map, exact a, ha, rfl⟩})
(λ a ha, rfl) (λ a ha, a.1, begin
  rcases finset.mem_map.mp ha with ⟨⟨w,ww⟩,hw,rfl⟩,
  change w < M,
end ⟩)
(λ a ha, finset.mem_univ _) (λ a ha, by tidy) (λ a ha, by tidy)

Johan Commelin (Jun 23 2021 at 17:58):

Do we have a version of finset.sum_bij' for injective maps. Since \iota is injective, I feel like the proof of the lemma should be a 1-liner

Johan Commelin (Jun 23 2021 at 18:02):

Nevermind: finset.sum_map

Last updated: Aug 03 2023 at 10:10 UTC