# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: If an equiv is contained with a set then so is its inverse

#### Eric Wieser (Jan 12 2021 at 10:00):

Does this exist? Is it true?

```
lemma equiv.inv_maps_to {s : set α} {f : perm α}
(h : set.maps_to f s s) : set.maps_to (f⁻¹ : _) s s :=
begin
unfold set.maps_to at *,
sorry
end
```

This came up in #5706, where a similar lemma is introduced that requires `fintype α`

. It's not clear to me whether this assumption is needed, but it's entirely possible I'm missing relevant intuition about finiteness

#### Anne Baanen (Jan 12 2021 at 10:07):

This should be true: the restriction of `f`

to `s`

is injective, so by finiteness of `s`

it is also surjective, therefore an equiv. The inverse restricted to `s`

is the inverse to the restriction of `f`

.

#### Eric Wieser (Jan 12 2021 at 10:07):

Ah, so the `fintype`

assumption is needed?

#### Anne Baanen (Jan 12 2021 at 10:08):

Yes, otherwise you can do things like mapping each rational number `x`

to `x / 2`

, which maps `[0, 1]`

to `[0, 1]`

but not in the other direction.

#### Eric Wieser (Jan 12 2021 at 10:08):

Thanks, a counter-example was exactly what I was hoping for. I should have looked for examples beyond nat and int...

#### Sebastien Gouezel (Jan 12 2021 at 10:23):

You have a counterexample in `int`

, with the addition of `1`

mapping the natural numbers to themselves, contrary to its inverse.

#### Eric Wieser (Jan 12 2021 at 10:44):

So in that example `α`

is `int`

, `f`

is the permutation which adds one, and `s`

is "non-negative"? Good point. I was slightly sad but not surprised to see that `slim_check`

couldn't help me here.

Last updated: May 07 2021 at 19:12 UTC