## 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