avewright/proofwiki-math huggingface dataset:
Theorem: Unit of Ring of Mappings iff Image is Subset of Ring Units

Let $\struct {R, +, \circ}$ be a ring with unity $1_R$.
Let $U_R$ be the set of units in $R$.
Let $S$ be a set.
Let $\struct {R^S, +', \circ'}$ be the ring of mappings on the set of mappings $R^S$.
Then:
:$f \in R^S$ is a unit of $R^S$ {{iff}} $\Img f \subseteq U_R$
where $\Img f$ is the image of $f$.
In this case, the inverse of $f$ is the mapping $f^{-1} : S \to U_R$ defined by:
:$\forall x \in S : \map {f^{-1} } x = \map f x^{-1}$

Proof:
From Structure Induced by Ring with Unity Operations is Ring with Unity, $\struct {R^S, +', \circ'}$ has a unity $f_{1_R}$ defined by:
:$\forall x \in S: \map {f_{1_R}} x = 1_R$
Theorem: Mapping is Bijection iff Composite with Direct Image Mapping with Complementation Commutes

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Then:
:$f$ is a bijection
{{iff}}:
:$f^\to \circ \complement_S = \complement_T \circ f^\to$
where:
:$f^\to: \powerset S \to \powerset T$ denotes the direct image mapping of $f$
:$\complement_S: \powerset S \to \powerset S$ denotes the complement relative to $S$
:$\complement_T: \powerset T \to \powerset T$ denotes the complement relative to $T$
:$\powerset S$ and $\powerset T$ denote the power sets of $S$ and $T$ respectively.

Proof:
=== Sufficient Condition ===
Let $f$ be a bijection.
Thus a fortiori $f$ is:
:a surjection
:a one-to-many relation
From One-to-Many Image of Set Difference: Corollary 2 we have:
:$\forall X \in \powerset S: \map {\paren {f^\to \circ \complement_S} } X = \map {\paren {\complement_{\Img f} \circ f^\to} } X$
By definition of surjection:
:$\Img f = T$
and so:
:$\forall X \in \powerset S: \map {\paren {f^\to \circ \complement_S} } X = \map {\paren {\complement_T \circ f^\to} } X$
That is:
:$f^\to \circ \complement_S = \complement_T \circ f^\to$
{{qed|lemma}}
Theorem: Relative Complement Mapping on Powerset is Bijection

Let $S$ be a set.
Let $\complement_S: \powerset S \to \powerset S$ denote the relative complement mapping on the power set of $S$.
Then $\complement_S$ is a bijection.
Thus each $T \subseteq S$ is in one-to-one correspondence with its relative complement.

Proof:
Let $f: \powerset S \to \powerset S$ be a mapping defined as:
:$\forall T \in \powerset S: \map f T = \relcomp S T$
It is to be demonstrated that $f$ is a bijection.
By definition of relative complement:
:$\relcomp S T = S \setminus T = \set {x \in S: x \notin T}$
and so it can be seen that $f$ is well-defined.
Let $T_1, T_2 \in \powerset S: \map f {T_1} = \map f {T_2}$.
Then:
{{begin-eqn}}
{{eqn | l = \map f {T_1}
      | r = \map f {T_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \relcomp S {T_1}
      | r = \relcomp S {T_2}
      | c = by definition of $f$
}}
{{eqn | ll= \leadsto
      | l = \relcomp S {\relcomp S {T_1} }
      | r = \relcomp S {\relcomp S {T_2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = T_1
      | r = T_2
      | c = Relative Complement of Relative Complement
}}
{{end-eqn}}
That is, $f$ is an injection.
Also:
{{begin-eqn}}
{{eqn | l = T
      | o = \in
      | r = \powerset S
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists X \in \powerset S
      | l = X
      | r = \relcomp S T
}}
{{eqn | ll= \leadsto
      | l = \relcomp S X
      | r = \relcomp S {\relcomp S T}
}}
{{eqn | ll= \leadsto
      | l = \relcomp S X
      | r = T
      | c = Relative Complement of Relative Complement
}}
{{end-eqn}}
That is, for all $T \in \powerset S$ there exists an $X$ such that $T = \map f X$.
This demonstrates that $f$ is a surjection.
The result follows by definition of bijection.
{{qed}}
Theorem: Power of One plus x in terms of Gaussian Hypergeometric Function

:$\map F {-p, 1; 1; -x} = \paren {1 + x}^p$

Proof:
{{begin-eqn}}
{{eqn | l = \map F {-p, 1; 1; -x}
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-p}^{\overline n} 1^{\overline n} } {1^{\overline n} } \frac {\paren {-x}^n} {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {\prod_{j \mathop = 0}^{n - 1} \paren {-p + j} } \frac {x^n} {n!}
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\prod_{j \mathop = 0}^{n - 1} \paren {-1} } \paren {\prod_{j \mathop = 0}^{n - 1} \paren {-p + j} } \frac {x^n} {n!}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\prod_{j \mathop = 0}^{n - 1} \paren {p - j} } \frac {x^n} {n!}
      | c = Product of Products
}}
{{eqn | r = \paren {1 + x}^p
      | c = General Binomial Theorem
}}
{{end-eqn}}
{{qed}}
Theorem: Logarithm of One plus x in terms of Gaussian Hypergeometric Function

:$\map \ln {1 + x} = x \map F {1, 1; 2; -x}$

Proof:
{{begin-eqn}}
{{eqn | l = x \map F {1, 1; 2; -x}
      | r = x \sum_{n \mathop = 0}^\infty \frac {\paren {1^{\overline n} }^2} {2^{\overline n} } \frac {\paren {-x}^n} {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {n!}^2 \paren {\frac {\paren {2 - 1}!} {\paren {2 + n - 1}!} } \frac {x^{n + 1} } {n!}
      | c = Rising Factorial as Quotient of Factorials, One to Integer Rising is Integer Factorial
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {n!}^2} {\paren {n + 1}! n!} x^{n + 1}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {\paren {n!}^2} {\paren {n + 1} \paren {n!}^2} x^{n + 1}
      | c = {{Defof|Factorial|index = 1}}
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n
      | c = shifting the index
}}
{{eqn | r = \map \ln {1 + x}
      | c = Power Series Expansion for $\map \ln {1 + x}$
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Exponential times Sine

:$\map {\laptrans {e^{b t} \sin a t} } s = \dfrac a {\paren {s - b}^2 + a^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {e^{b t} \sin a t} } s
      | r = \map {\laptrans {\sin a t} } {s - b}
      | c = First Translation Property of Laplace Transforms
}}
{{eqn | r = \frac a {\paren {s - b}^2 + a^2}
      | c = Laplace Transform of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Exponential times Cosine

:$\map {\laptrans {e^{b t} \cos a t} } s = \dfrac {s - b} {\paren {s - b}^2 + a^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {e^{b t} \cos a t} } s
      | r = \map {\laptrans {\cos a t} } {s - b}
      | c = First Translation Property of Laplace Transforms
}}
{{eqn | r = \frac {s - b} {\paren {s - b}^2 + a^2}
      | c = Laplace Transform of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Direct Image Mapping of Injection equals Direct Image of Complement

Let $f: S \to T$ be an injection.
Let $f^\to: \powerset S \to \powerset T$ denote the direct image mapping of $f$.
Then:
:$\forall A \in \powerset S: \map {\paren {\complement_{\Img f} \circ f^\to} } A = \map {\paren {f^\to \circ \complement_S} } A$
where $\circ$ denotes composition of mappings.

Proof:
As $f$ is an injection, it is a fortiori a one-to-many relation.
From Image of Set Difference under Relation: Corollary 2:
:$\forall A \in \powerset S: \map {\paren {\complement_{\Img \RR} \circ \RR^\to} } A = \map {\paren {\RR^\to \circ \complement_S} } A$
where $\RR \subseteq S \times T$ is a one-to-many relation on $S \times T$.
Substituting $f$ for $\RR$ gives the result:
:$\forall A \in \powerset S: \map {\paren {\complement_{\Img f} \circ f^\to} } A = \map {\paren {f^\to \circ \complement_S} } A$
{{Qed}}
Theorem: Direct Image of Inverse Image of Direct Image equals Direct Image Mapping

Let $f: S \to T$ be a mapping.
Let:
:$f^\to: \powerset S \to \powerset T$ denote the direct image mapping of $f$
:$f^\gets: \powerset T \to \powerset S$ denote the inverse image mapping of $f$
where $\powerset S$ denotes the power set of $S$.
Then:
:$f^\to \circ f^\gets \circ f^\to = f^\to$
where $\circ$ denotes composition of mappings.

Proof:
{{begin-eqn}}
{{eqn | q = \forall A \in \powerset S
      | l = A
      | o = \subseteq
      | r = \map {\paren {f^\gets \circ f^\to} } A
      | c = Subset of Domain is Subset of Preimage of Image
}}
{{eqn | ll= \leadsto
      | q = \forall A \in \powerset S
      | l = \map {f^\to} A
      | o = \subseteq
      | r = \map {\paren {f^\to \circ f^\gets \circ f^\to} } A
      | c = Image of Subset under Mapping is Subset of Image
}}
{{eqn-intertext|and:}}
{{eqn | q = \forall B \in \powerset T
      | l = \map {\paren {f^\to \circ f^\gets} } B
      | o = \subseteq
      | r = B
      | c = Subset of Codomain is Superset of Image of Preimage
}}
{{eqn | ll= \leadsto
      | q = \forall A \in \powerset S
      | l = \map {\paren {f^\to \circ f^\gets} } {\map {f^\to} A}
      | o = \subseteq
      | r = \map {f^\to} A
      | c = Image of Subset under Mapping is Subset of Image, setting $B = \map {f^\to} A \in \powerset T$
}}
{{end-eqn}}
Thus we have:
:$\forall A \in \powerset S: \map {f^\to} A \subseteq \map {\paren {f^\to \circ f^\gets \circ f^\to} } A \subseteq \map {f^\to} A$
and the result follows.
{{qed}}
Theorem: Inverse Image of Direct Image of Inverse Image equals Inverse Image Mapping

Let $f: S \to T$ be a mapping.
Let:
:$f^\to: \powerset S \to \powerset T$ denote the direct image mapping of $f$
:$f^\gets: \powerset T \to \powerset S$ denote the inverse image mapping of $f$
where $\powerset S$ denotes the power set of $S$.
Then:
:$f^\gets \circ f^\to \circ f^\gets = f^\gets$
where $\circ$ denotes composition of mappings.

Proof:
{{begin-eqn}}
{{eqn | q = \forall A \in \powerset S
      | l = A
      | o = \subseteq
      | r = \map {\paren {f^\gets \circ f^\to} } A
      | c = Subset of Domain is Subset of Preimage of Image
}}
{{eqn | ll= \leadsto
      | q = \forall B \in \powerset T
      | l = \map {f^\gets} B
      | o = \subseteq
      | r = \map {\paren {f^\gets \circ f^\to} } {\map {f^\gets} B}
      | c = Image of Subset under Mapping is Subset of Image, setting $A = \map {f^\gets} B \in \powerset S$
}}
{{eqn-intertext|and:}}
{{eqn | q = \forall B \in \powerset T
      | l = \map {\paren {f^\to \circ f^\gets} } B
      | o = \subseteq
      | r = B
      | c = Subset of Codomain is Superset of Image of Preimage
}}
{{eqn | ll= \leadsto
      | q = \forall A \in \powerset S
      | l = \map {\paren {f^\gets \circ f^\to \circ f^\gets} } B
      | o = \subseteq
      | r = \map {f^\gets} B
      | c = Image of Subset under Mapping is Subset of Image
}}
{{end-eqn}}
Thus we have:
:$\forall B \in \powerset T: \map {f^\gets} B \subseteq \map {\paren {f^\gets \circ f^\to \circ f^\gets} } B \subseteq \map {f^\gets} B$
and the result follows.
{{qed}}
Theorem: Direct Image of Intersection with Inverse Image

Then:
:$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$

Proof:
Let $A \in \powerset S, B \in \powerset T$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map {f^\to} {A \cap \map {f^\gets} B}
      | o = \subseteq 
      | r = \map {f^\to} A \cap \map {f^\to} {\map {f^\gets} B}
      | c = Image of Intersection under Mapping
}}
{{eqn | o = \subseteq 
      | r = \map {f^\to} A \cap B
      | c = Subset of Codomain is Superset of Image of Preimage
}}
{{end-eqn}}
Let $x \in \map {f^\to} A \cap B$.
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {f^\to} A
      | c = {{Defof|Set Intersection}}
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = x
      | r = \map f a
      | c = for some $a \in A$
}}
{{eqn-intertext|and:}}
{{eqn | l = x
      | o = \in
      | r = B
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = \map f a
      | o = \in
      | r = B
      | c = from $(1)$ above
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \in
      | r = \map {f^\gets} B
      | c = {{Defof|Inverse Image Mapping}}
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \in
      | r = A \cap \map {f^\gets} B
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | l = \map f a
      | o = \in
      | r = \map {f^\to} {A \cap \map {f^\gets} B}
      | c = {{Defof|Direct Image Mapping}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \map {f^\to} {A \cap \map {f^\gets} B}
      | c = as $x = \map f a$
}}
{{eqn | ll= \leadsto
      | l = \map {f^\to} A \cap B
      | o = \subseteq
      | r = \map {f^\to} {A \cap \map {f^\gets} B}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Thus we have:
:$\map {f^\to} {A \cap \map {f^\gets} B} \subseteq \map {f^\to} A \cap B$
and:
:$\map {f^\to} A \cap B \subseteq \map {f^\to} {A \cap \map {f^\gets} B}$
and so:
:$\forall A \in \powerset S, B \in \powerset T: \map {f^\to} {A \cap \map {f^\gets} B} = \map {f^\to} A \cap B$
by definition of set equality.
{{qed}}
Theorem: Graph of Real Function in Cartesian Plane intersects Vertical at One Point

Let $f: \R \to \R$ be a real function.
Let its graph be embedded in the Cartesian plane $\CC$:
:520px
Every vertical line through a point $a$ in the domain of $f$ intersects the graph of $f$ at exactly one point $P = \tuple {a, \map f a}$.

Proof:
From Equation of Vertical Line, a vertical line in $\CC$ through the point $\tuple {a, 0}$ on the $x$-axis has an equation $x = a$.
A real function is by definition a mapping.
Hence:
:$\forall a_1, a_2 \in \Dom f: a_1 = a_2 \implies \map f {a_1} = \map f {a_2}$
where $\Dom f$ denotes the domain of $f$.
Thus for each $a \in \Dom f$ there exists exactly one ordered pair $\tuple {a, y}$ such that $y = \map f a$.
That is, there is exactly one point on $x = a$ which is also on the graph of $f$.
The result follows.
{{qed}}
Theorem: Equation of Vertical Line

Let $\LL$ be a vertical line embedded in the Cartesian plane $\CC$.
Then the equation of $\LL$ can be given by:
:$x = a$
where $\tuple {a, 0}$ is the point at which $\LL$ intersects the $x$-axis.
:520px

Proof:
From the Normal Form of Equation of Straight Line in Plane, a general straight line can be expressed in the form:
:$x \cos \alpha + y \sin \alpha = p$
where:
:$p$ is the length of a perpendicular $\PP$ from $\LL$ to the origin.
:$\alpha$ is the angle made between $\PP$ and the $x$-axis.
As $\LL$ is vertical, then by definition $\PP$ is horizontal.
By definition, the horizontal line through the origin is the $x$-axis itself.
Thus $\alpha = 0$ and $p = a$
Hence the equation of $\LL$ becomes:
{{begin-eqn}}
{{eqn | l = x \cos 0 + y \sin 0
      | r = a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = a
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equation of Horizontal Line

Let $\LL$ be a horizontal line embedded in the Cartesian plane $\CC$.
Then the equation of $\LL$ can be given by:
:$y = b$
where $\tuple {0, b}$ is the point at which $\LL$ intersects the $y$-axis.
:520px

Proof:
From the Normal Form of Equation of Straight Line in Plane, a general straight line can be expressed in the form:
:$x \cos \alpha + y \sin \alpha = p$
where:
:$p$ is the length of a perpendicular $\PP$ from $\LL$ to the origin
:$\alpha$ is the angle made between $\PP$ and the $x$-axis.
As $\LL$ is horizontal, then by definition $\PP$ is vertical.
By definition, the vertical line through the origin is the $y$-axis itself.
Thus:
:$\alpha$ is a right angle, that is $\alpha = \dfrac \pi 2 = 90 \degrees$
:$p = b$
Hence the equation of $\LL$ becomes:
{{begin-eqn}}
{{eqn | l = x \cos \dfrac \pi 2 + y \sin \dfrac \pi 2
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \times 0 + y \times 1
      | r = b
      | c = Sine of Right Angle, Cosine of Right Angle
}}
{{eqn | ll= \leadsto
      | l = y
      | r = b
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Unit of Ring of Mappings iff Image is Subset of Ring Units/Image is Subset of Ring Units implies Unit of Ring of Mappings

Let $\struct {R, +, \circ}$ be a ring with unity $1_R$.
Let $U_R$ be the set of units in $R$.
Let $S$ be a set.
Let $\struct {R^S, +', \circ'}$ be the ring of mappings on the set of mappings $R^S$.
Let $\Img f \subseteq U_R$ where $\Img f$ is the image of $f$.
Then:
:$f \in R^S$ is a unit of $R^S$
and the inverse of $f$ is the mapping $f^{-1} : S \to U_R$ defined by:
:$\forall x \in S : \map {f^{-1}} {x} = \map f x^{-1}$

Proof:
By assumption: 
:$\forall x \in S: \exists \map f x^{-1} : \map f x \circ \map f x^{-1} = \map f x^{-1} \circ \map f x  = 1_R$
Let $f^{-1} : S \to U_R$ be defined by:
:$\forall x \in S : \map {f^{-1}} {x} = \map f x^{-1}$
Consider the mapping $f \circ’ f^{-1}$.
For all $x \in S$: 
{{begin-eqn}}
{{eqn | l = \map {\paren {f \circ’ f^{-1} } } x
      | r = \map f x \circ’ \map {f^{-1} } x
}}
{{eqn | r = \map f x \circ \map f x^{-1}
}}
{{eqn | r = 1_R
}}
{{end-eqn}}
Hence $f \circ’ f^{-1} = f_{1_R}$.
Similarly, $f^{-1} \circ’ f = f_{1_R}$.
Hence $f$ is a unit of $\struct {R^S, +', \circ'}$ and the inverse of $f$ is the mapping $f^{-1}$.
Theorem: Unit of Ring of Mappings iff Image is Subset of Ring Units/Unit of Ring of Mappings implies Image is Subset of Ring Units

Let $\struct {R, +, \circ}$ be a ring with unity $1_R$.
Let $U_R$ be the set of units in $R$.
Let $S$ be a set.
Let $\struct {R^S, +', \circ'}$ be the ring of mappings on the set of mappings $R^S$.
Let $f \in R^S$ be a unit of $R^S$.
Then:
:$\Img f \subseteq U_R$
where $\Img f$ is the image of $f$.
In which case, the inverse of $f$ is the mapping $f^{-1} : S \to U_R$ defined by:
:$\forall x \in S : \map {f^{-1} } x = \map f x^{-1}$

Proof:
Let $f^{-1}$ be the product inverse of $f$.
Let $x \in R$.
Then:
{{begin-eqn}}
{{eqn | l = 1_R 
      | r = \map {f_{1_R} } x
      | c = Structure Induced by Ring with Unity Operations is Ring with Unity
}}
{{eqn | r = \map {\paren {f \circ' f^{-1} } } x
      | c = {{Defof|Product Inverse|product inverse}}
}}
{{eqn | r = \map f x \circ \map {f^{-1} } x
      | c = {{Defof|Pointwise Operation}} $\circ'$
}}
{{end-eqn}}
Similarly, $1_R = \map {f^{-1} } x \circ \map f x$
Hence $\map {f^{-1}} x$ is the product inverse of $\map f x$.
So $\map f x$ is a unit in $R$ and $\map f x^{-1} = \map {f^{-1} } x$.
The result follows.
Theorem: Graph of Real Surjection in Coordinate Plane intersects Every Horizontal Line

Let $f: \R \to \R$ be a real function which is surjective.
Let its graph be embedded in the Cartesian plane $\CC$:
:520px
Every horizontal line through a point $b$ in the codomain of $f$ intersects the graph of $f$ on at least one point $P = \tuple {a, b}$ where $b = \map f a$.

Proof:
From Equation of Horizontal Line, a horizontal line in $\CC$ through the point $\tuple {0, b}$ on the $y$-axis has an equation $y = b$.
By hypothesis, $f$ is a surjection.
Hence:
:$\forall b \in \R: \exists a \in \R: b = \map f a$
Thus for each $b \in \R$ there exists at least one ordered pair $\tuple {a, b}$ such that $b = \map f a$.
That is, there exists at least one point on $y = b$ which is also on the graph of $f$.
The result follows.
{{qed}}
Theorem: Graph of Real Injection in Coordinate Plane intersects Horizontal Line at most Once

Let $f: \R \to \R$ be a real function which is injective.
Let its graph be embedded in the Cartesian plane $\CC$:
:520px
Let $\LL$ be a horizontal line through a point $b$ in the codomain of $f$.
Then $\LL$ intersects the graph of $f$ on at most one point $P = \tuple {a, b}$ where $b = \map f a$.

Proof:
From Equation of Horizontal Line, a horizontal line in $\CC$ through the point $\tuple {0, b}$ on the $y$-axis has an equation $y = b$.
By hypothesis, $f$ is a injection.
Hence:
:$\forall a_1, a_2 \in \Dom f: \map f {a_1} = \map f {a_2} \implies a_1 = a_2$
where $\Dom f$ denotes the domain of $f$.
Thus for each $b \in \Cdm f$ there exists exactly one ordered pair $\tuple {a, b}$ such that $b = \map f a$.
That is, there is exactly one point on $y = b$ which is also on the graph of $f$.
The result follows.
{{qed}}
Theorem: Graph of Real Bijection in Coordinate Plane intersects Horizontal Line at One Point

Let $f: \R \to \R$ be a real function which is bijective.
Let its graph be embedded in the Cartesian plane $\CC$:
:520px
Every horizontal line through a point $b$ in the codomain of $f$ intersects the graph of $f$ on exactly one point $P = \tuple {a, b}$ where $b = \map f a$.

Proof:
By definition, a bijection is a mapping which is both an injection and a surjection.
Let $\LL$ be a horizontal line through a point $b$ in the codomain of $f$.
From Graph of Real Surjection in Coordinate Plane intersects Every Horizontal Line:
:$\LL$ intersects the graph of $f$ on at least one point $P = \tuple {a, b}$ where $b = \map f a$.
From Graph of Real Injection in Coordinate Plane intersects Horizontal Line at most Once:
:$\LL$ intersects the graph of $f$ on at most one point $P = \tuple {a, b}$ where $b = \map f a$.
The result follows.
{{qed}}
Theorem: Composite of Surjection on Injection is not necessarily Either

Let $f$ be an injection.
Let $g$ be a surjection.
Let $g \circ f$ denote the composition of $g$ with $f$.
Then it is not necessarily the case that $g \circ f$ is either a surjection or an injection.

Proof:
Let $X, Y, Z$ be sets defined as:
{{begin-eqn}}
{{eqn | l = X
      | r = \set {a, b, c}
      | c = 
}}
{{eqn | l = Y
      | r = \set {1, 2, 3, 4}
      | c = 
}}
{{eqn | l = Z
      | r = \set {z, y, z}
      | c = 
}}
{{end-eqn}}
Let $f: X \to Y$ be defined in two-row notation as:
:$\dbinom {a \ b \ c } {1 \ 2 \ 3}$
which is seen by inspection to be an injection.
Let $g: Y \to Z$ be defined in two-row notation as:
:$\dbinom {1 \ 2 \ 3 \ 4} {x \ y \ y \ z}$
which is seen by inspection to be a surjection.
The composition $f \circ g$ is seen to be:
:$\dbinom {a \ b \ c} {x \ y \ y}$
which is:
:not an injection (both $b$ and $c$ map to $y$)
:not a surjection (nothing maps to $z$).
Hence the result.
{{qed}}
Category:Injections
Category:Surjections
Category:Composite Mappings
pr38md0rxug63sezves2glotq8qwr01
Theorem: Composition of 3 Mappings where Pairs of Mappings are Bijections

Let $A$, $B$, $C$ and $D$ be sets.
Let:
:$f: A \to B$
:$g: B \to C$
:$h: C \to D$
be mappings.
Let $g \circ f$ and $h \circ g$ be bijections.
Then $f$, $g$ and $h$ are all bijections.

Proof:
We note that both $g \circ f$ and $h \circ g$ are both injections and surjections by definition of bijection.
First it is shown that $g$ is a bijection.
We are given that:
:$g \circ f$ is a bijection.
From Injection if Composite is Injection it follows that $f$ is an injection.
From Surjection if Composite is Surjection it follows that $g$ is a surjection.
Similarly, we are given that:
:$h \circ g$ is a bijection.
From Injection if Composite is Injection it follows that $g$ is an injection.
From Surjection if Composite is Surjection it follows that $h$ is a surjection.
Thus we have that $g$ is a bijection.
{{qed|lemma}}
Next it is shown that $f$ is a bijection.
{{AimForCont}} $f$ is not a surjection.
Then:
:$\exists y \in B: \neg \exists x \in A: \map f x = y$
But then $g$ is a surjection and so:
:$\forall z \in C: \exists y \in B: z = \map g y$
and so:
:$\exists z \in C: \neg \exists x \in A: \map g {\map f x} = z$
and so $g \circ f$ is not a surjection.
This contradicts our assertion that $g \circ f$ is a bijection and so a surjection.
Hence by Proof by Contradiction $f$ must be a surjection
So $f$ is both an injection and a surjection, and so a bijection.
{{qed|lemma}}
Next it is shown that $h$ is a bijection.
{{AimForCont}} $h$ is not an injection.
Then:
:$\exists y_1, y_2 \in C: \map h {y_1} = \map h {y_2}$
But then $g$ is a bijection and so:
:$\exists x_1, x_2 \in B: y_1 = \map g {x_1} \ne \map g {x_2} = y_2$
and so:
:$\exists x_1, x_2 \in B: \map h {\map g {x_1} } = \map h {\map g {x_2} }$
and so $h \circ g$ is not an injection.
This contradicts our assertion that $h \circ g$ is a bijection and so an injection.
Hence by Proof by Contradiction $h$ must be an injection
So $h$ is both an injection and a surjection, and so a bijection.
{{qed|lemma}}
Hence the result.
{{qed}}