# Zulip Chat Archive

## Stream: maths

### Topic: finset puzzle

#### Kevin Buzzard (Jan 24 2020 at 18:41):

import data.finset example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β] (f : α → finset β) : finset.bind s f = finset.sup s f := sorry -- or to put it another way example (α : Type*) (β : Type*) [decidable_eq β] : @finset.bind α β _ = @finset.sup (finset β) α _ := sorry

There are two different ways to take a finite union of finite sets. Trying to prove directly that they are equal seems hard to me -- but am I missing something? Perhaps one should prove instead that they have the same elements?

#### Johan Commelin (Jan 24 2020 at 18:42):

Yes, use `ext`

#### Kevin Buzzard (Jan 24 2020 at 18:45):

This came up when I was trying to prove this:

import data.mv_polynomial example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} [decidable_eq σ] : mv_polynomial.vars p = p.support.bind finsupp.support := sorry

`vars`

is something in the `mv_polynomial`

API which I had not come across until the other day, but its interface seems very basic. Chris' instinct was to use `bind`

to do unions like this -- but apparently it wasn't Johannes'. Of course as long as the API is there it doesn't matter, but when Chris proved for me that evaluating a polynomial at two different assignments of the variables which agree on the variables of the polynomial will give the same answer, he used bind and it came out really nicely.

#### Kevin Buzzard (Jan 24 2020 at 18:46):

gaargh, `finset.mem_sup`

is not there because it's working in some arbitrary lattice

#### Kevin Buzzard (Jan 24 2020 at 18:48):

⊢ (∃ (i : α) (H : i ∈ s), a ∈ f i) ↔ a ∈ finset.sup s f

is what I'm left with

#### Kevin Buzzard (Jan 24 2020 at 18:49):

the sup is defined as a fold over union.

#### Johan Commelin (Jan 24 2020 at 18:49):

Is there a `mem_fold`

?

#### Kevin Buzzard (Jan 24 2020 at 18:50):

I just don't know whether I'm supposed to be digging this low. All I want to prove is that evaluating a polynomial at two different assignments which agree on all the variables of the polynomial gives the same answer :-)

#### Johan Commelin (Jan 24 2020 at 18:50):

So, sorry the statement and feed it to an UG at xena (-;

#### Kevin Buzzard (Jan 24 2020 at 18:53):

There's no `mem_fold`

anywhere. I could prove it by induction I guess :-/ But when I launched into a proof the other day involving evaluations of mv_polynomials, Mario just came along and proved it with a very well-judged `simp`

, and at Xena on Thursday when we were proving that the evaluations were equal if the assignments agreed on the support (as defined by `bind`

) Chris stopped at some point and said "automation should do it from here". I am not sure I understand the full power of `simp`

with these things.

#### Kevin Buzzard (Jan 24 2020 at 19:00):

oh I see what to do -- there is sup_le and le_sup and those should give it me.

#### Kevin Buzzard (Jan 24 2020 at 19:30):

gaargh `le_sup`

isn't enough. I'm left with

1 goal α : Type u_1, s : finset α, β : Type u_2, _inst_2 : decidable_eq β, f : α → finset β, x : β, hx : x ∈ finset.sup s f ⊢ ∃ (a : α) (H : a ∈ s), x ∈ f a

#### Floris van Doorn (Jan 24 2020 at 19:57):

Here is a proof assuming decidable equality on `\a`

:

import data.finset example (α : Type*) (s : finset α) (β : Type*) [decidable_eq α] [decidable_eq β] (f : α → finset β) : finset.bind s f = finset.sup s f := finset.induction_on s rfl (λ x s hx IH, by simp [IH])

#### Floris van Doorn (Jan 24 2020 at 20:07):

And here is a proof without that assumption:

import data.finset example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β] (f : α → finset β) : finset.bind s f = finset.sup s f := begin apply le_antisymm, { intro y, rw finset.mem_bind, rintro ⟨x, hx, hy⟩, have := @finset.le_sup _ _ _ _ f _ hx, exact this hy }, { refine finset.sup_le _, intros x hx y hy, rw finset.mem_bind, exact ⟨x, hx, hy⟩ } end

#### Floris van Doorn (Jan 24 2020 at 20:08):

You indeed also need `sup_le`

.

#### Kevin Buzzard (Jan 24 2020 at 21:36):

Thanks a lot Floris. What frustrates me is that I still can't do an arbitrary puzzle like this immediately. Mulling things over I wondered whether it was worth proving that if you had a predicate on lattices with the property that P(x union y) was true iff P(x) or P(y) was true then some statement about sups was true

#### Kevin Buzzard (Jan 24 2020 at 21:37):

True for sup iff true for one of the elements. Need P(bot) false too

#### Kevin Buzzard (Jan 24 2020 at 22:01):

@Floris van Doorn do you think it's crazy to prove the `vars`

question and I should instead just re-define mv_polynomial.vars? Chris seemed to think that the bind version was much easier to work with. See for example his (untidied) proof of the thing I needed yesterday: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Algebraic.20geometry.20course/near/186420269

#### Mario Carneiro (Jan 25 2020 at 00:34):

@Floris van Doorn Here's a shorter proof without the assumption:

example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β] (f : α → finset β) : finset.bind s f = finset.sup s f := by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH])

#### Kevin Buzzard (Jan 25 2020 at 01:12):

Thanks Mario. Can you prove @Chris Hughes ' `vars`

defined via the bind is the same as @Johannes Hölzl's '?

#### Mario Carneiro (Jan 25 2020 at 01:30):

theorem finset.bind_eq_sup {α β} [decidable_eq β] (s : finset α) (f : α → finset β) : finset.bind s f = finset.sup s f := by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH]) @[simp] theorem multiset.union_to_finset {α} [decidable_eq α] (s t : multiset α) : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset := by ext a; simp theorem multiset.sup_to_finset (α : Type*) (s : finset α) (β : Type*) [decidable_eq β] (f : α → multiset β) : (finset.sup s f).to_finset = finset.bind s (λ x, (f x).to_finset) := by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH]) example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} [decidable_eq σ] : mv_polynomial.vars p = p.support.bind finsupp.support := begin unfold mv_polynomial.vars mv_polynomial.degrees, rw multiset.sup_to_finset, congr, funext x, apply finsupp.to_finset_to_multiset, end

#### Kevin Buzzard (Jan 30 2020 at 14:10):

A belated thanks for this Mario!

Last updated: May 09 2021 at 10:11 UTC