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: Dec 20 2023 at 11:08 UTC