# Zulip Chat Archive

## Stream: new members

### Topic: finset ignorance

#### Patrick Lutz (Aug 19 2020 at 03:52):

I realized I don't understand how I am supposed to do the following with finsets. Suppose that I have a type `X`

which I'd like to prove is finite. Suppose that I already have a proof of this which goes as follows: starting with some type `Y`

and some subsets `s`

and `t`

of `Y`

which I know are finite, I can construct a surjective map `s × t → X`

. If I want to rewrite this proof to use some equivalent definition of `s`

and `t`

where they are finsets instead of just subsets of `Y`

, how do I do that? When I try to write `s × t → X`

, Lean complains to me about the type of `s`

and `t`

being `finset Y`

rather than `Type u`

.

#### Patrick Lutz (Aug 19 2020 at 03:52):

The situation where this came up is a little complicated so I have just tried to describe the source of my confusion. I can try to make a mwe if it would be helpful.

#### Mario Carneiro (Aug 19 2020 at 03:53):

is it possible to express the function as simply Y -> Y -> X?

#### Patrick Lutz (Aug 19 2020 at 03:54):

Sure

#### Patrick Lutz (Aug 19 2020 at 03:55):

But I get the same error when I do that

#### Patrick Lutz (Aug 19 2020 at 03:56):

I.e. when I write `s → t → X`

, Lean tells me that it expected something of type `Type u`

but got something of type `finset Y`

instead

#### Mario Carneiro (Aug 19 2020 at 03:56):

so something like this?

```
example {X Y} (f : Y → Y → X) (s t : finset Y)
(h : ∀ z, ∃ (x ∈ s) (y ∈ t), f x y = z) : fintype X := sorry
```

#### Patrick Lutz (Aug 19 2020 at 03:57):

Mario Carneiro said:

is it possible to express the function as simply Y -> Y -> X?

Oops, I misread this.

#### Patrick Lutz (Aug 19 2020 at 03:58):

It's probably possible to write it as `Y -> Y -> X`

but it would be a bit annoying

#### Mario Carneiro (Aug 19 2020 at 03:58):

why? what's the real setting

#### Patrick Lutz (Aug 19 2020 at 03:58):

For instance I don't actually know whether `X`

is nonempty

#### Mario Carneiro (Aug 19 2020 at 03:59):

Is `X`

also a subset of a bigger type?

#### Patrick Lutz (Aug 19 2020 at 03:59):

Mario Carneiro said:

Is

`X`

also a subset of a bigger type?

Yeah

#### Patrick Lutz (Aug 19 2020 at 04:00):

This is not quite true, but it's basically the set of certain linear combinations of the roots of two polynomials

#### Mario Carneiro (Aug 19 2020 at 04:00):

is it a submodule or something like that?

#### Patrick Lutz (Aug 19 2020 at 04:00):

No

#### Patrick Lutz (Aug 19 2020 at 04:01):

Not all linear combinations, just a few of them

#### Patrick Lutz (Aug 19 2020 at 04:02):

Actually it's a little bit worse than that. I have two fields `F`

and `E`

and `E`

is a field extension of `F`

(expressed by saying `E`

is an `F`

-algebra) and `X`

is the set of elements of `F`

which can be written in a certain way as a linear combination of the roots of two polynomials over `E`

#### Patrick Lutz (Aug 19 2020 at 04:03):

and `s`

and `t`

are basically the roots of the polynomials

#### Patrick Lutz (Aug 19 2020 at 04:03):

The surjection is pretty easy to construct when I just define `s`

and `t`

directly as subsets of `E`

. But I want to use `polynomial.roots`

instead

#### Mario Carneiro (Aug 19 2020 at 04:04):

So like this then?

```
example {S Y} (s t : finset Y) (X : set S) (f : Y → Y → S)
(h : ∀ z ∈ X, ∃ (x ∈ s) (y ∈ t), f x y = z) : set.finite X := sorry
```

#### Mario Carneiro (Aug 19 2020 at 04:05):

I'm just trying to get a sense of what kind of hypothesis would be easiest for you to work with

#### Patrick Lutz (Aug 19 2020 at 04:10):

that's pretty close, but it's more like `X`

is actually a subset of `T`

and there's some injective map `g : T -> S`

and the hypothesis is `forall z \in X, \exists (x \in s) (y \in t), f x y = g z`

#### Patrick Lutz (Aug 19 2020 at 04:10):

Mario Carneiro said:

So like this then?

`example {S Y} (s t : finset Y) (X : set S) (f : Y → Y → S) (h : ∀ z ∈ X, ∃ (x ∈ s) (y ∈ t), f x y = z) : set.finite X := sorry`

I'd be happy to just know the best way to do this though

#### Mario Carneiro (Aug 19 2020 at 04:13):

I would express it as "the subset of the image of the product of finite sets is finite"

#### Mario Carneiro (Aug 19 2020 at 04:13):

and `h`

is the proof that it's a subset

#### Mario Carneiro (Aug 19 2020 at 04:18):

```
example {S Y} (s t : finset Y) (X : set S) (f : Y → Y → S)
(h : ∀ z ∈ X, ∃ x y, (x ∈ s ∧ y ∈ t) ∧ f x y = z) : set.finite X :=
begin
refine (set.finite.image (λ z:Y×Y, f z.1 z.2) (set.finite_mem_finset (s.product t))).subset _,
simpa [set.subset_def] using h,
end
```

#### Kenny Lau (Aug 19 2020 at 06:52):

@Patrick Lutz it is an essential skill to be able to extract the essence of a lemma, i.e. remove all the noise about field extensions and state it as a lemma about sets and functions

#### Patrick Lutz (Aug 19 2020 at 06:52):

Kenny Lau said:

Patrick Lutz it is an essential skill to be able to extract the essence of a lemma, i.e. remove all the noise about field extensions and state it as a lemma about sets and functions

So I'm learning.

#### Kevin Buzzard (Aug 19 2020 at 08:56):

You can promote a finset to a set and then to a type if you want to take those products

Last updated: May 13 2021 at 05:21 UTC