# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Preimage of finite sets

#### Adam Topaz (Jun 06 2020 at 18:40):

Hi everyone. I'm looking for the statement that the preimage under an *injective map* of a finite subset is finite, using `finset`

. So, approximately something like this:

```
import data.finset
open function
example {S : Type*} {T : Type*} {f : S → T} {h : injective f} {F : finset T} :
∃ G : finset S, f ⁻¹' ↑F = ↑G := sorry
```

Does mathlib have anything close to this?

#### Kevin Buzzard (Jun 06 2020 at 19:21):

There is indeed no mention of `comap`

in `finset.lean`

.

#### Kevin Buzzard (Jun 06 2020 at 19:24):

`finset.lean`

has `map`

and `image`

but no `comap`

. This would be a neat little PR unless I have completely missed something.

#### Kevin Buzzard (Jun 06 2020 at 19:25):

`finset.lean`

must have been written by a bunch of amateurs

#### Kevin Buzzard (Jun 06 2020 at 19:29):

Oh golly there is not even `multiset.comap`

#### Kevin Buzzard (Jun 06 2020 at 19:33):

Yeah this is all a bit crazy. `finset.map`

is defined only for embeddings, when it could be defined in general; `finset.comap`

, which does need embeddings, is missing. `multiset.map`

is correctly defined for all maps. @Mario Carneiro if it was decided that `finset.map`

was worth writing over 20 lemmas for in the special case where the map was an embedding, would the same apply for `multiset.comap`

and `finset.comap`

?

#### Adam Topaz (Jun 06 2020 at 19:33):

Does something like this exist?

```
import data.finset
open function
open_locale classical
example {S : Type*} {T : Type*} {f : S → T} {F : finset T} :
∃ G : finset S, finset.image f G = F := sorry -- WRONG
```

Presumably this would be enough...

#### Kevin Buzzard (Jun 06 2020 at 19:34):

That's not true unless f is surjective

#### Patrick Massot (Jun 06 2020 at 19:34):

Kevin, are you missing https://github.com/leanprover-community/mathlib/blob/e48c2af4f2f92c2331a912c588610db73085939d/src/data/finset.lean#L1225?

#### Adam Topaz (Jun 06 2020 at 19:34):

Oh ovbiously... I should take an intersection with the image (and I don't know how to do that...)

#### Kevin Buzzard (Jun 06 2020 at 19:34):

We're going the other way Patrick (I think)

#### Kevin Buzzard (Jun 06 2020 at 19:35):

Aah but I see what you're saying. That's a `map`

with no injectivity assumption

#### Kevin Buzzard (Jun 06 2020 at 19:36):

Just to be clear Adam, the issue is not how to define the function, the issue is whether it is already in mathlib

#### Adam Topaz (Jun 06 2020 at 19:37):

Yeah I know... I've just haven't used finsets before so it is an issue for me :)

#### Johan Commelin (Jun 06 2020 at 19:37):

#### Kevin Buzzard (Jun 06 2020 at 19:39):

So it is there, but in `set.finite`

, and it's called `preimage`

not `comap`

.

#### Adam Topaz (Jun 06 2020 at 19:46):

While we're here, is there something like this? (which should have been what I wrote above):

```
import data.finset
open function
open_locale classical
example {S : Type*} {T : Type*} {f : S → T} {F : finset T} :
↑F ⊆ set.range f → ∃ G : finset S, finset.image f G = F := sorry
```

#### Kevin Buzzard (Jun 06 2020 at 19:50):

This you'll need the axiom of choice for.

#### Adam Topaz (Jun 06 2020 at 19:50):

I'm happy with that...

#### Kevin Buzzard (Jun 06 2020 at 19:51):

Oh -- you can do better than `f '' set.univ`

-- we have `image f`

.

#### Adam Topaz (Jun 06 2020 at 19:52):

Which namespace is that in?

#### Adam Topaz (Jun 06 2020 at 19:52):

Or am I missing some import?

#### Kevin Buzzard (Jun 06 2020 at 19:54):

oh sorry! It's called `range f`

#### Kevin Buzzard (Jun 06 2020 at 19:54):

#### Adam Topaz (Jun 06 2020 at 19:55):

Thanks! I updated the code.

#### Kevin Buzzard (Jun 06 2020 at 19:55):

It's easier to use because you don't have to prove that `x \in univ`

.

#### Kevin Buzzard (Jun 06 2020 at 19:56):

It wouldn't surprise me if this is not in the library, and my idea for how to do it is kind of a horrible mess.

#### Adam Topaz (Jun 06 2020 at 20:08):

It's not slick, and I don't know enough of the library to quickly fill in the sorry's, but here is a sketch -- is this what you had in mind?

```
import data.finset
open function
open_locale classical
example {S : Type*} {T : Type*} {f : S → T} {F : finset T} :
↑F ⊆ set.range f→ ∃ G : finset S, finset.image f G = F :=
begin
refine finset.induction_on F _ _,
{
intro h,
use ∅,
trivial,
},
{
intros a U ha ind sur,
have h1 : ↑U ⊆ set.range f, by sorry, -- from sur
have h2 : ∃ s : S, f s = a, by sorry, -- from sur
cases ind h1 with G hG,
cases h2 with s hs,
use insert s G,
rw [finset.image_insert, hs],
refine congr_arg (insert a) hG,
}
end
```

#### Kevin Buzzard (Jun 06 2020 at 20:16):

```
have h1 : ↑U ⊆ set.range f,
{ intros x hx, apply sur, simp [hx]},
```

#### Kevin Buzzard (Jun 06 2020 at 20:18):

```
have h2 : ∃ s : S, f s = a,
{ show a ∈ set.range f,
apply sur,
simp},
```

#### Kevin Buzzard (Jun 06 2020 at 20:19):

I don't know whether this `apply sur`

is mathlib-approved, but `X \sub Y`

is sugar for `forall a, a \in X -> a \in Y`

so you can just `apply sur`

like a function

#### Adam Topaz (Jun 06 2020 at 20:19):

You beat me to it :)

I got this:

```
import data.finset
open function
open_locale classical
example {S : Type*} {T : Type*} {f : S → T} {F : finset T} :
↑F ⊆ set.range f→ ∃ G : finset S, finset.image f G = F :=
begin
refine finset.induction_on F _ _,
{
intro h,
use ∅,
trivial,
},
{
intros a U ha ind sur,
have h1 : ↑U ⊆ set.range f,
{ intros x hx, apply sur, simp [hx]},
have h2 : ∃ s : S, f s = a,
{
suffices : a ∈ ↑(insert a U), by exact @sur a this,
simp,
},
cases ind h1 with G hG,
cases h2 with s hs,
use insert s G,
rw [finset.image_insert, hs],
refine congr_arg (insert a) hG,
}
end
```

Last updated: May 17 2021 at 16:26 UTC