Zulip Chat Archive

Stream: maths

Topic: Product of `univ : finset (option α)`


view this post on Zulip Anne Baanen (Mar 02 2020 at 13:35):

What is the best approach to proving the following goal:

example {α β : Type} {x : α} {v : β  α} [comm_monoid α] [fintype β] :
  finset.univ.prod (λ (i : option β), i.elim x v) = x * finset.univ.prod v :=
sorry

I guess finset.sum_insert would be the first step?

view this post on Zulip Johan Commelin (Mar 02 2020 at 13:42):

I would show that univ : finset (option β) is the same as insert none (erase none univ)

view this post on Zulip Johan Commelin (Mar 02 2020 at 13:42):

After that, I think there are enough library lemmas to just follow your nose.

view this post on Zulip Johan Commelin (Mar 02 2020 at 13:43):

(Just a guess...) If you get stuck, then you've certainly found a hole in the library.

view this post on Zulip Patrick Massot (Mar 02 2020 at 13:49):

I can't even parse the statement. Can someone translate this into LaTeX for me?

view this post on Zulip Chris Hughes (Mar 02 2020 at 13:50):

What is LateX for option.none?

view this post on Zulip Patrick Massot (Mar 02 2020 at 13:50):

I guess it depends on context.

view this post on Zulip Chris Hughes (Mar 02 2020 at 13:50):

Here's a proof.

calc univ.prod (λ (i : option β), i.elim x v)
    = x * (univ.erase (none)).prod (λ (i : option β), i.elim x v) :
  begin
    conv_lhs { rw [ insert_erase (mem_univ (none : option β))] },
    rw [prod_insert (not_mem_erase _ _)], refl
  end
... = x * finset.univ.prod v :
  begin
    refine congr_arg2 _ rfl (prod_bij (λ a _, some a) _ _ _ _).symm,
    { simp },
    { intros, refl },
    { simp },
    { assume b,
      cases b with b,
      { simp },
      { intro, use b, simp } }
  end

view this post on Zulip Patrick Massot (Mar 02 2020 at 13:51):

I think I understand the statement now.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 14:00):

Here's a proof.

but where's your proof that it's the best approach? ;-)

view this post on Zulip Anne Baanen (Mar 02 2020 at 14:00):

Ah, prod_bij is what I was missing!

view this post on Zulip Anne Baanen (Mar 02 2020 at 14:01):

Would it be worth it to include this in mathlib (as a @[simp] lemma)?

view this post on Zulip Chris Hughes (Mar 02 2020 at 14:01):

prod_bij is really handy. We need docs that say things like prod_bij is how you prove a lot of things about products.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 14:06):

Patrick Massot said:

I can't even parse the statement. Can someone translate this into LaTeX for me?

It says xiβv(i)=xiβv(i)x\prod_{i\in\beta}v(i)=x\prod_{i\in\beta}v(i)

view this post on Zulip Patrick Massot (Mar 02 2020 at 14:08):

That translation explains why this is a hard Lean problem. Empty math implies hard Lean almost surely.

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 14:09):

Nice proof Chris. This is exactly, I guess, why one needs prod_bij: it says "the products over two sets that mathematicians might not be able to tell the difference between, are equal"

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 14:10):

(deleted)


Last updated: May 06 2021 at 18:20 UTC