## Stream: Beginner Questions

### Topic: Inverse of bijective function

#### Nicolò Cavalleri (Jun 23 2021 at 23:32):

Suppose I have a lemma proving that a given function is bijective. How do I define the inverse function? In my real life problem I actually have a function f which satisfies bij_betw f UNIV (S :: 'b set) and I need to build a function 'b => 'a such that it is the inverse if f on S. Can I do this?

#### Jakub Kądziołka (Jun 23 2021 at 23:34):

see the_inv_into

#### Nicolò Cavalleri (Jun 24 2021 at 12:13):

Thank you! I am puzzled though: how does that definition work? If f is not surjective the inverse is not unique, and f is never assumed surjective, so how does THE work? My guess is that it uses some very powerful axiom of choice...

#### Jakub Kądziołka (Jun 24 2021 at 12:50):

THE is a variation on Hilbert's epsilon operator, which is present in Isabelle as SOME. SOME indeed corresponds to the axiom of choice, and is defined as follows: if EX x. P x, then SOME returns some x that has the property, otherwise an arbitrary x from your type. THE additionally requires that there is exactly one x st. P x, which, means the happy case doesn't require AC, as it corresponds to a function {x} \mapsto x, which should be constructible in ZF? Though, the case where ALL x. P x = False corresponds to undefined :: 'a, and I'm not sure whether that's AC or not...

#### Manuel Eberl (Jun 24 2021 at 19:02):

THE is the unique choice operator, and its existence is actually "weaker" than that of the existence of the SOME operator (non-unique choice). But I'll leave the precise explanation of what that means to people who actually know something about logic (in contrast to me).

#### Nicolò Cavalleri (Jun 24 2021 at 19:03):

Bu my point is precisely that if the function is not surjective the inverse is not unique! In fact I was very surprised to see a THE there

#### Manuel Eberl (Jun 24 2021 at 19:06):

In that case you just get some unspecified value that you can prove nothing about (cf. undefined).

#### Nicolò Cavalleri (Jun 24 2021 at 19:06):

You mean in the case the function is not surjetive?

#### Manuel Eberl (Jun 24 2021 at 19:07):

HOL cannot prevent you from writing down "nonsense". There are a number of terms that are "nonsensical" in some sense, e.g. 1 / 0. Some of them have some halfway sensible dummy values like 1 / 0 = 0, others are just unspecified (e.g. ln (-1 :: real) or THE x. False).

#### Manuel Eberl (Jun 24 2021 at 19:10):

Nicolò Cavalleri said:

You mean in the case the function is not surjetive?

The way the_inv_into is defined, the_inv_into A f y is the unique value x such that x ∈ A and f(x) = y if such a unique value exists; otherwise you get "nonsense".

#### Manuel Eberl (Jun 24 2021 at 19:11):

If the function is not injective and surjective, there will be some values y where the_inv_into A f y will be "nonsense" (i.e. unspecified). It might still work for other values of y though if the choice is unique.

#### Nicolò Cavalleri (Jun 24 2021 at 19:11):

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

#### Manuel Eberl (Jun 24 2021 at 19:11):

For instance, if $f(x) = x^2$, then the_inv_into UNIV f 0 = 0. For anything other than 0, it's unspecified.

#### Manuel Eberl (Jun 24 2021 at 19:12):

Nicolò Cavalleri said:

But then what if I have an injective function of which I want a right inverse? Isn't there a theory of inverse functions that makes use of SOME? In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Yes, there is inv_into. Frankly I've never used the_inv_into; I didn't even know it existed.

#### Manuel Eberl (Jun 24 2021 at 19:12):

I don't think there is any reason to ever use the_inv_into over inv_into.

#### Manuel Eberl (Jun 24 2021 at 19:13):

inv_into also works if the value is not unique, it's enough for the preimage to be nonempty.

#### Nicolò Cavalleri (Jun 24 2021 at 19:13):

Oh great then I was looking for inv_into I guess!

#### Manuel Eberl (Jun 24 2021 at 19:13):

Nicolò Cavalleri said:

In any case I am puzzled that in lemmas involving the_inv_into you often see the hypothesis that the function be injective but never that it be surjective...

Do you have any examples?

#### Nicolò Cavalleri (Jun 24 2021 at 19:13):

Manuel Eberl said:

I don't think there is any reason to ever use the_inv_into over inv_into.

Yep I don't see it either!

#### Manuel Eberl (Jun 24 2021 at 19:13):

I guess surjectivity is generally an unnecessarily strong assumption.

#### Manuel Eberl (Jun 24 2021 at 19:14):

It's enough for the specific values you're plugging into the the_inv_into to be in the image of A under f, i.e. in fA`.

Last updated: Sep 25 2021 at 09:17 UTC