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

Stream: Is there code for X?

[Eric Wieser]

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]

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]

Ah, so the fintype assumption is needed?

[Anne Baanen]

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]

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

[Sebastien Gouezel]

You have a counterexample in int, with the addition of 1 mapping the natural numbers to themselves, contrary to its inverse.

[Eric Wieser]

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.