Are my conjecture and proof below mathematically and linguistically correct?
Are they well formulated?
How can they be improved?
How can they be shortened?
Is the conjecture obviously?
As far as I know, the theorem and its topic are new. A confirmation of usefulness and applicability of the theorem is at the end of this question.
Clearly, part a) of the conjecture is trivial, but it's good for the application of the theorem if part a) is written down together with the non-trivial cases.
Definition:
Let $S$ a set. A function $f$ is called a ''function in the set $S$'', if $f\colon\mathrm{dom}(f)\subseteq S\to S$.
Conjecture:
Let
$S_\alpha,S$ sets with $S_\alpha\subseteq S$,
$\alpha\in S_\alpha$,
$f$ a non-empty function in the set $S$,
$F$ a set of functions in the set $S$,
$F_{bij}(\alpha)$ the set of the function values of all bijective functions from $F$ defined at $\alpha$,
$z$ solution variable.
Let the equation $f(z)=\alpha$ be given.
a) If the equation has more than one solution, then $f$ has no inverse function.
b) If the equation has at least one solution $z_0\notin F_ {bij}(\alpha)$ for $z$, then $f$ has no inverse function in $F$.
c) If $\alpha$ is a function value of $f$ and the equation has no solution $z_0\in F_{bij}(\alpha)$ for $z$, then $f$ has no inverse function in $F$.
Proof:
We consider the equation from the conjecture and its solutions $z_0$:
$$f(z_0)=\alpha.\tag{1}$$
If $z_0\notin\mathrm{dom}(f)$, then $f(z_0)$ doesn't exist, then $z_0$ is not a solution to the equation.
If $\alpha\notin f(\mathrm{dom}(f))$, then $z_0\notin\mathrm{dom}(f)$, then $z_0$ is, according to the above, not a solution to the equation.
So, the equation only has solutions if $z_0\in\mathrm{dom}(f)$ and $\alpha\in f(\mathrm{dom}(f))$.
If the equation has solutions, then the solutions are arguments of $f$ and $\alpha $ is the image of the solutions under the function $f$.
Proof of part a) of the conjecture
According to the precondition of part a) of the conjecture, equation (1) has more than one solution. Then, according to what has just been said, $\alpha$ is the image of more than one argument of $f$. So $f$ is not injective and therefore not bijective. It follows that $f$ has no inverse function. This proves part a) of the conjecture.
Proof of part b) of the conjecture
According to the precondition of part b) of the conjecture, equation (1) has at least one solution.
If the equation has more than one solution, then $f$ has no inverse function, according to part a) of the conjecture. Then $f$ has no inverse function in $F$.
Equation (1) now has exactly one solution $z_0$.
We carry out a proof by contradiction.
Assume $f$ has an inverse function $f^{-1}$ in $F$. Then the function value $z_0=f^{-1}(\alpha)$ of the function $f^{-1}$ would exist, $f^{-1}$ would be bijective and therefore $z_0\in F_ {bij}(\alpha)$. This contradicts the assumption $z_0\notin F_ {bij}(\alpha)$ of the conjecture. So the assumption was wrong. It follows that $f$ has no inverse function in $F$.
This proves part b) of the conjecture.
Proof of part c) of the conjecture
According to the precondition of part c) of the conjecture, $\alpha$ is a function value of $f$.
We carry out a proof by contradiction.
Assume $f$ has an inverse function $f^{-1}$ in $F$. Then the function value $z_0=f^{-1}(\alpha)$ of the function $f^{-1}$ would exist. Because then $f(z_0)=\alpha$, $z_0$ would be a solution to equation (1). In addition, $f^{-1}$ would be bijective and therefore $z_0\in F_{bij}(\alpha)$. This contradicts the assumption of the conjecture that the equation has no solution $z_0\in F_{bij}(\alpha)$. So the assumption was wrong. It follows that $f$ has no inverse function in $F$. This proves part c) of the conjecture.
This proves the conjecture.
Justification of usefulness of the theorem:
The theorem can be applied for deciding the non-existence of inverses in a given class of functions, e.g. in the Elementary functions with the field of constants $\mathbb{Q}$ (see e.g. the definition of the Elementary functions
in [Ritt 1925] or [Ritt 1948]) or in terms of some Special functions, e.g. in closed form.
I want to show that the non-existence of inverses in some classes of functions follows from the non-existence of particular solutions of particular equations in some cases.
(As far as I know, this knowledge is new.)
Start by fixing a set $F$ of functions.
Take as a first example e.g. the Elementary functions as defined in [Ritt 1925] for $F$, the Elementary numbers as defined in [Lin 1983] for $S_\alpha$, and $S=\mathbb{C}$.
Take the equation of the main theorem of [Lin 1983] and apply the above conjecture.
Consider that the Elementary numbers are generated from the Integers by applying finite numbers of elementary functions and that the Elementary numbers are closed under application of finite numbers of elementary functions (elementary functions with the above mentioned definition). So, an elementary function maps elementary values to all of its elementary arguments. And the same holds for an elementary inverse.
$\ $
[Ritt 1948] Ritt, J. F.: Integration in finite terms. Liouville's theory of elementary methods. Columbia University Press, New York, 1948
Best Answer
I didn't check your proofs in detail but I think they are correct.
You asked:
Yes, I think it is.