avewright/proofwiki-math huggingface dataset:
Theorem: Right Operation is Entropic

The right operation is entropic:
:$\forall a, b, c, d: \paren {a \to b} \to \paren {c \to d} = \paren {a \to c} \to \paren {b \to d}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a \to b} \to \paren {c \to d}
      | r = b \to d
      | c = {{Defof|Right Operation}}
}}
{{eqn | r = d
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {a \to c} \to \paren {b \to d}
      | r = c \to d
      | c = {{Defof|Right Operation}}
}}
{{eqn | r = d
      | c = 
}}
{{eqn | r = \paren {a \to b} \to \paren {c \to d}
      | c = {{apriori}}
}}
{{end-eqn}}
{{qed}}
Theorem: Entropic Structure with Identity is Commutative Monoid

Let $\struct {S, \odot}$ be a magma.
Let $\struct {S, \odot}$ be an entropic structure:
:$\forall a, b, c, d \in S: \paren {a \odot b} \odot \paren {c \odot d} = \paren {a \odot c} \odot \paren {b \odot d}$
Let $\struct {S, \odot}$ have an identity element $e$.
Then $\struct {S, \odot}$ is a commutative monoid.

Proof:
We have that $\struct {S, \odot}$ is a magma.
Thus {{afortiori}} $\struct {S, \odot}$ is closed, and {{MonoidAxiom|0}} is fulfilled.
Then:
{{begin-eqn}}
{{eqn | q = \forall a, b, c \in S
      | l = \paren {a \odot b} \odot c
      | r = \paren {a \odot b} \odot \paren {e \odot c}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {a \odot e} \odot \paren {b \odot c}
      | c = {{Defof|Entropic Structure}}
}}
{{eqn | r = a \odot \paren {b \odot c}
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Thus $\odot$ is an associative operation and {{MonoidAxiom|1}} is fulfilled.
We are given that $e$ is an identity element for $\struct {S, \odot}$.
Hence {{MonoidAxiom|2}} is fulfilled {{hypothesis}}.
Thus we have that $\struct {S, \odot}$ is a monoid.
Then:
{{begin-eqn}}
{{eqn | q = \forall a, b \in S
      | l = a \odot b
      | r = \paren {e \odot a} \odot \paren {b \odot e}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {e \odot b} \odot \paren {a \odot e}
      | c = {{Defof|Entropic Structure}}
}}
{{eqn | r = b \odot a
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Thus $\struct {S, \odot}$ is a commutative monoid.
{{qed}}
Theorem: Linear Combination Operator on Real Numbers is Entropic

Let $a, b \in \R$ be real numbers.
Let $\odot$ be the operation on $\R$ defined as:
:$\forall x, y \in \R: x \odot y := a x + b y$
Then $\odot$ is an entropic operation.

Proof:
{{begin-eqn}}
{{eqn | q = \forall p, q, r, s \in \R
      | l = \paren {p \odot q} \odot \paren {r \odot s}
      | r = a \paren {a p + b q} + b \paren {a r + b s}
      | c = Definition of $\odot$
}}
{{eqn | r = a^2 p + a b q + b a r + b^2 s
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = a^2 p + a b r + b a q + b^2 s
      | c = Real Multiplication is Commutative and Real Addition is Commutative
}}
{{eqn | r = a \paren {a p + b r} + b \paren {a q + b s}
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \paren {p \odot r} \odot \paren {q \odot s}
      | c = Real Multiplication Distributes over Addition
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Closed Subsets of Power Structure of Entropic Structure is Closed

Let $\struct {S, \odot}$ be a magma.
Let $\struct {S, \odot}$ be an entropic structure.
Let $\struct {\powerset S, \odot_\PP}$ be the power structure of $\struct {S, \odot}$.
Let $\TT$ be the set of all submagmas of $\struct {S, \odot}$.
Then the algebraic structure $\struct {\TT, \odot_\PP}$ is a submagma of $\struct {\powerset S, \odot_\PP}$ which is itself an entropic structure.

Proof:
Recall the definition of subset product:
:$A \odot_\PP B = \set {a \odot b: \tuple {a, b} \in A \times B}$
First we show that:
:$\forall A, B \in \TT: A \odot_\PP B \in \TT$
Let $A$ and $B$ be arbitrary elements of $\TT$.
Let $a$ and $c$ be arbitrary elements of $A$.
Let $b$ and $d$ be arbitrary elements of $B$.
Then we have:
{{begin-eqn}}
{{eqn | l = a \odot b
      | o = \in
      | r = A \odot_\PP B
      | c = {{Defof|Subset Product}}
}}
{{eqn | l = c \odot d
      | o = \in
      | r = A \odot B
      | c = {{Defof|Subset Product}}
}}
{{eqn | l = a \odot c
      | o = \in
      | r = A
      | c = as $\struct {A, \odot}$ is closed
}}
{{eqn | l = b \odot d
      | o = \in
      | r = B
      | c = as $\struct {B, \odot}$ is closed
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \paren {a \odot b} \odot \paren {c \odot d}
      | r = \paren {a \odot c} \odot \paren {b \odot d}
      | c = {{Defof|Entropic Structure}}
}}
{{eqn | o = \in
      | r = A \odot_\PP B
      | c = {{apriori}}: $a \odot c \in A$, $b \odot d \in B$
}}
{{end-eqn}}
That is:
:$A \odot_\PP B$ is closed in $S$.
As $A$ and $B$ are arbitrary, it follows that $\struct {\TT, \odot_\PP}$ is closed in $\powerset S$.
{{qed|lemma}}
Then we need to show that:
:$\forall A, B, C, D \in \TT: \paren {A \odot_\PP B} \odot_\PP \paren {C \odot_\PP D} = \paren {A \odot_\PP C} \odot_\PP \paren {B \odot_\PP D}$
demonstrating the entropic nature of $\struct {\TT, \odot_\PP}$.
We have:
{{begin-eqn}}
{{eqn | q = \forall A, B, C, D \in \TT
      | o = 
      | r = \paren {A \odot_\PP B} \odot_\PP \paren {C \odot_\PP D}
      | c = 
}}
{{eqn | r = \set {\paren {a \odot b} \odot \paren {c \odot d}: a \in A, b \in B, c \in C, d \in  D}
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \set {\paren {a \odot c} \odot \paren {b \odot d}: a \in A, b \in B, c \in C, d \in  D}
      | c = {{Defof|Entropic Structure}} $\struct {S, \odot}$ is entropic
}}
{{eqn | r = \paren {A \odot_\PP C} \odot_\PP \paren {B \odot_\PP D}
      | c = {{Defof|Subset Product}}
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Substructure of Entropic Structure is Entropic

Let $\struct {S, \odot}$ be an entropic structure:
:$\forall a, b, c, d \in S: \paren {a \odot b} \odot \paren {c \odot d} = \paren {a \odot c} \odot \paren {b \odot d}$
Let $\struct {T, \odot_T}$ be a substructure of $\struct {S, \odot}$.
Then $\struct {T, \odot_T}$ is also an entropic structure.

Proof:
{{begin-eqn}}
{{eqn | q = \forall a, b, c, d \in T
      | o = 
      | r = \paren {a \odot_T b} \odot_T \paren {c \odot_T d}
      | c = 
}}
{{eqn | r = \paren {a \odot b} \odot \paren {c \odot d}
      | c = {{Defof|Operation Induced by Restriction}}
}}
{{eqn | r = \paren {a \odot c} \odot \paren {b \odot d}
      | c = as $S$ is an entropic structure
}}
{{eqn | r = \paren {a \odot_T c} \odot_T \paren {b \odot_T d}
      | c = {{Defof|Operation Induced by Restriction}}
}}
{{end-eqn}}
{{qed}}
Category:Entropic Structures
inn8q3c8pz3d1o3oj1xvwsna2737sxb
Theorem: Quotient Epimorphism Condition for Normal Subgroup Product to be Internal Group Direct Product

Let $\struct {G, \odot}$ be a group
Let $\struct {H, \odot}$ and $\struct {K, \odot}$ be normal subgroups of $\struct {G, \odot}$.
Then:
:$\struct {G, \odot}$ is the internal group direct product of $\struct {H, \odot}$ and $\struct {K, \odot}$
{{iff}}
:the restriction of the quotient epimorphism $q_H$ to $K$ is an isomorphism from $K$ onto the quotient group $G / H$
and:
:the restriction of the quotient epimorphism $q_K$ to $H$ is an isomorphism from $H$ onto the quotient group $G / K$

Proof:
=== Sufficient Condition ===
{{:Quotient Epimorphism Condition for Normal Subgroup Product to be Internal Group Direct Product/Sufficient Condition}}{{qed|lemma}}
Theorem: Restriction of Homomorphism is Homomorphism

Let $\struct {S, \circ}$ and $\struct {T, \odot}$ be algebraic structures.
Let $\phi: S \to T$ be a homomorphism.
Let $A \subseteq S$ be a subset of $S$.
Then the restriction of $\phi$ to $A \times \Img A$ is also a homomorphism.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x, y \in A
      | l = \map \phi {x \circ{\restriction_{A} } y}
      | r = \map \phi {x \circ y}
      | c = {{Defof|Restriction of Operation}}
}}
{{eqn | r = \map \phi x \odot \map \phi y
      | c = {{Defof|Homomorphism (Abstract Algebra)}}
}}
{{eqn | r = \map \phi x \odot {\restriction_{\Img A} } \map \phi y
      | c = {{Defof|Restriction of Operation}}
}}
{{end-eqn}}
{{qed}}
Category:Homomorphisms (Abstract Algebra)
Category:Restrictions
hx5nypm0vyqgyc8irr1ccb29sfmlgvw
Theorem: Composition of Mappings is Right Distributive over Pointwise Operation

Let $A$ and $B$ be sets.
Let $\struct {S, \odot}$ be an algebraic structure.
Let:
:$B^A$ denote the set of mappings from $A$ to $B$
:$S^B$ denote the set of mappings from $B$ to $S$.
Let $f, g \in S^B$ be mappings from $B$ to $S$.
Let $h \in B^A$ be a mapping from $A$ to $B$.
Then:
:$\paren {f \odot g} \circ h = \paren {f \circ h} \odot \paren {g \circ h}$
where:
:$f \odot g$ denotes the pointwise operation on $S^B$ induced by $\odot$
:$g \circ h$ denotes the composition of $g$ with $h$.

Proof:
First we establish:
The domain of $h$ is $A$.
The codomain of $h$ is $B$
The domain of both $f$ and $g$ is $B$.
The codomain of both $f$ and $g$ is $S$.
Hence:
:the domain of $\paren {f \odot g} \circ h$ is $A$
:the Domain of $f \odot g$ is $B$
:the codomain of $f \odot g$ is $S$
:the codomain of $\paren {f \odot g} \circ h$ is $S$.
Then:
:the domain of $f \circ h$ is $A$
:the domain of $g \circ h$ is $A$
:the codomain of $f \circ h$ is $S$
:the codomain of $g \circ h$ is $S$
:the domain of $\paren {f \circ h} \odot \paren {g \circ h}$ is $A$
:the codomain of $\paren {f \circ h} \odot \paren {g \circ h}$ is $S$.
Hence both $\paren {f \odot g} \circ h$ and $\paren {f \circ h} \odot \paren {g \circ h}$ have the same domain and codomain.
Let $a \in A$ be arbitrary.
Let $b \in B$ be such that $b = \map h a$. 
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {\paren {f \odot g} \circ h} } a
      | r = \map {\paren {f \odot g} } {\map h a}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\paren {f \odot g} } b
      | c = Definition of $b$
}}
{{eqn | r = \map f b \odot \map g b
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f {\map h a} \odot \map g {\map h a}
      | c = Definition of $b$
}}
{{eqn | r = \map {\paren {f \circ h} } a \odot \map {\paren {g \circ h} } a
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\paren {\paren {f \circ h} \odot \paren {g \circ h} } } a
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
Hence the result by Equality of Mappings.
{{qed}}
Theorem: Composition of Mappings is Left Distributive over Homomorphism of Pointwise Operation

Let $A$ be a set.
Let $\struct {S, \odot}$ and $\struct {T, \otimes}$ be algebraic structures.
Let:
:$S^A$ denote the set of mappings from $A$ to $S$.
Let $f$ be a homomorphism from $S$ to $T$.
Let $g, h \in S^A$ be mappings from $A$ to $S$.
Then:
:$f \circ \paren {g \odot h} = \paren {f \circ g} \otimes \paren {f \circ h}$
where:
:$g \odot h$ denotes the pointwise operation on $S^A$ induced by $\odot$
:$f \circ h$ denotes the composition of $f$ with $h$.

Proof:
First we establish:
The domain of $g$ and $h$ is $A$.
The codomain of $g$ and $h$ is $S$.
The domain of $f$ is $S$.
The codomain of $f$ is $T$.
Hence:
:the Domain of $g \odot h$ is $A$
:the codomain of $g \odot h$ is $S$
:the domain of $f \circ \paren {g \odot h}$ is $A$
:the codomain of $f \circ \paren {g \odot h}$ is $T$.
Then:
:the domain of $f \circ g$ is $A$
:the domain of $f \circ h$ is $A$
:the codomain of $f \circ g$ is $S$
:the codomain of $f \circ h$ is $S$
:the domain of $\paren {f \circ g} \otimes \paren {f \circ h}$ is $A$
:the codomain of $\paren {f \circ g} \otimes \paren {f \circ h}$ is $T$.
Hence both $f \circ \paren {g \odot h}$ and $\paren {f \circ g} \otimes \paren {f \circ h}$ have the same domain and codomain.
Let $a \in A$ be arbitrary.
Let $b \in B$ be such that $b = \map g a$. 
Let $c \in B$ be such that $c = \map h a$.
Let $d \in T$ such that $d = b \odot c$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \circ \paren {g \odot h} } } a
      | r = \map f {\map {\paren {g \odot h} } a}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map f {\paren {\map g a \odot \map h a} }
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f {\paren {b \odot c} }
      | c = Definition of $b$ and $c$
}}
{{eqn | r = \paren {\map f b} \otimes \paren {\map f c}
      | c = as $f$ is a homomorphism
}}
{{eqn | r = \paren {\map f {\map g a} } \otimes \paren {\map f {\map h a} }
      | c = Definition of $b$ and $c$
}}
{{eqn | r = \paren {\map {\paren {f \circ g} } a} \otimes \paren {\map {\paren {f \circ h} } a}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \map {\paren {\paren {f \circ g} \otimes \paren {f \circ h} } } a
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
Hence the result by Equality of Mappings.
{{qed}}
Theorem: Isomorphism between Algebraic Structures induces Isomorphism between Induced Structures

Let $A$ be a set.
Let $\struct {S, \odot}$ and $\struct {T, \otimes}$ be algebraic structures.
Let:
:$S^A$ denote the set of mappings from $A$ to $S$
:$T^A$ denote the set of mappings from $A$ to $T$.
Let:
:$\struct {S^A, \odot}$ denote the algebraic structure on $S^A$ induced by $\odot$
:$\struct {T^A, \otimes}$ denote the algebraic structure on $T^A$ induced by $\otimes$.
Let $\phi$ be an isomorphism from $S$ to $T$.
Let $\chi: S^A \to T^A$ be the mapping defined as:
:$\forall f \in S^A: \map \chi f = \phi \circ f$
where:
:$\phi \circ f$ denotes the composition of $\phi$ with $f$.
Then:
:$\chi$ is an isomorphism from $\struct {S^A, \odot}$ to $\struct {T^A, \otimes}$

Proof:
Let $f: A \to S$ and $g: A \to S$ be arbitrary elements of $S^A$.
We have that $\phi$ is an isomorphism.
Hence $\phi$ is {{afortiori}} a homomorphism which is a bijection.
Hence, from Bijection iff exists Mapping which is Left and Right Inverse, $\phi$ has an inverse mapping $\phi^{-1}: T \to S$ such that:
:$\phi \circ \phi^{-1} = I_T$
:$\phi^{-1} \circ \phi = I_S$
where $I_S$ and $I_T$ denote the identity mappings on $S$ and $T$ respectively.
From Inverse of Bijection is Bijection, $\phi^{-1}$ is also a bijection.
We have that:
{{begin-eqn}}
{{eqn | l = \map \chi {f \odot g}
      | r = \phi \circ \paren {f \odot g}
      | c = Definition of $\chi$
}}
{{eqn | r = \paren {\phi \circ f} \otimes \paren {\phi \circ g}
      | c = Composition of Mappings is Left Distributive over Homomorphism of Pointwise Operation
}}
{{eqn | r = \map \chi f \otimes \map \chi g
      | c = Definition of $\chi$
}}
{{end-eqn}}
demonstrating that $\chi$ is a homomorphism.
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = \map \chi f
      | r = \map \chi g
      | c = by assumption
}}
{{eqn | ll= \leadsto
      | l = \phi \circ f
      | r = \phi \circ g
      | c = Definition of $\chi$
}}
{{eqn | ll= \leadsto
      | l = \phi^{-1} \circ \phi \circ f
      | r = \phi^{-1} \circ \phi \circ g
      | c = as $\phi$ is a bijection 
}}
{{eqn | ll= \leadsto
      | l = f
      | r = g
      | c =  
}}
{{end-eqn}}
Hence $\chi$ is an injection.
{{qed|lemma}}
Let $g: A \to T$ be an arbitrary element of $T^A$.
As $\phi^{-1}: T \to S$ is a bijection:
:$\exists h \in S^A: h = \map {\phi^{-1} } g = \phi^{-1} \circ g$
That is:
:$\exists h \in S^A: \map \phi h = g$
As $g$ is arbitrary:
:$\forall g \in T^A: \exists h \in S^A: g = \phi \circ h = \map \chi h$
That is, $\chi$ is a surjection.
{{qed|lemma}}
We have shown that $\chi$ is:
:an injection
:a surjection
:a homomorphism
and so by definition $\chi$ is an isomorphism.
{{qed}}
Theorem: Vitali Set Existence Theorem/Lemma

For all real numbers in the closed unit interval $\mathbb I = \closedint 0 1$, define the relation $\sim$ such that:
:$\forall x, y \in \mathbb I: x \sim y \iff x - y \in \Q$
where $\Q$ is the set of rational numbers.
That is, $x \sim y$ {{iff}} their difference is rational.
Then $\sim$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Induced Structure from Doubleton is Isomorphic to External Direct Product with Self

Let $A$ be a set.
Let $\struct {S, \odot}$ be an algebraic structure.
Let $S^A$ denote the set of mappings from $A$ to $S$.
Let $\struct {S^A, \odot}$ denote the algebraic structure on $S^A$ induced by $\odot$.
Then $\struct {S^A, \odot}$ is isomorphic to the external direct product of $\struct {S, \odot}$ with itself.

Proof:
Let $A = \set {a, b}$ where $a$ and $b$ are arbitrary.
Let $\phi: S^A \to S^2$ be defined as:
:$\forall f \in S^A: \map \phi f = \tuple {\map f a, \map f b}$
We are to show that $\phi$ is an isomorphism.
First we demonstrate that $\phi$ is a homomorphism.
So, let $f, g \in S^A$.
Recall that:
:by definition of pointwise operation:
::$\forall f, g \in S^A: \map {\paren {f \odot g} } x = \map f x \odot \map g x$
:by definition of external direct product:
::$\forall \tuple {x_1, x_2}, \tuple {y_1, y_2} \in S \times S: \tuple {x_1, x_2} \odot \tuple {y_1, y_2} = \tuple {x_1 \odot y_1, x_2 \odot y_2}$
We have:
{{begin-eqn}}
{{eqn | l = \map \phi {f \odot g}
      | r = \tuple {\map {\paren {f \odot g} } a, \map {\paren {f \odot g} } b}
      | c = Definition of $\phi$
}}
{{eqn | r = \tuple {\map f a \odot \map g a, \map f b \odot \map g b}
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \tuple {\map f a, \map f b} \odot {\map g a, \map g b}
      | c = {{Defof|External Direct Product}}
}}
{{eqn | r = \map \phi f \odot \map \phi g
      | c = Definition of $\phi$
}}
{{end-eqn}}
and so $\phi$ has been shown to be a homomorphism.
{{qed|lemma}}
It remains to be shown that $\phi$ is a bijection.
Let $\map \phi f = \map \phi g$.
We have:
{{begin-eqn}}
{{eqn | l = \map \phi f
      | r = \map \phi g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {\map f a, \map f b}
      | r = \tuple {\map g a, \map g b}
      | c = Definition of $\phi$
}}
{{eqn | ll= \leadsto
      | l = \map f a
      | r = \map g a
      | c = Equality of Ordered Pairs
}}
{{eqn | lo= \land
      | l = \map f b
      | r = \map g b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = f
      | r = g
      | c = Equality of Mappings
}}
{{end-eqn}}
Thus by definition $\phi$ is an injection.
Let $\tuple {s_1, s_2} \in S$ be arbitrary.
By the nature of $S^A$, there exists a mapping $h: A \to S$ such that:
:$\map h a = s_1$
:$\map h b = s_2$
Hence:
:$\map \phi h = \tuple {s_1, s_2}$
As $\tuple {s_1, s_2}$ is arbitrary, it follows that $\phi$ is a surjection.
Thus $\phi$ is both an injection and a surjection, hence by definition a bijection.
{{qed|lemma}}
We have that $\phi$ is a homomorphism which is a bijection.
That is, $\phi$ is an isomorphism.
The result follows.
{{qed}}
Theorem: Structure Induced on Set of Self-Maps on Entropic Structure is Entropic

Let $\struct {S, \odot}$ be a magma.
Let $\struct {S, \odot}$ be an entropic structure.
Let $S^S$ be the set of all mappings from $S$ to itself.
Let $\struct {S^S, \oplus}$ denote the algebraic structure on $S^S$ induced by $\odot$.
Then $\struct {S^S, \oplus}$ is an entropic structure.

Proof:
Recall the definition of algebraic structure on $S^S$ induced by $\odot$:
Let $f: S \to S$ and $g: S \to S$ be self-maps on $S$, and thus elements of $S^S$.
The pointwise operation on $S^S$ induced by $\odot$ is defined as:
:$\forall x \in S: \map {\paren {f \oplus g} } x = \map f x \odot \map g x$
Let $f, g, p, q \in S^S$ be arbitrary.
Let $x \in S$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {\paren {f \oplus g} \oplus \paren {p \oplus q} } } x
      | r = \paren {\map f x \odot \map g x} \odot \paren {\map p x \odot \map q x}
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren {\map f x \odot \map p x} \odot \paren {\map g x \odot \map q x}
      | c = {{Defof|Entropic Structure}}
}}
{{eqn | r = \map {\paren {\paren {f \oplus p} \oplus \paren {g \oplus q} } } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | ll= \leadsto
      | l = \paren {f \oplus g} \oplus \paren {p \oplus q}
      | r = \paren {f \oplus p} \oplus \paren {g \oplus q}
      | c = Equality of Mappings
}}
{{end-eqn}}
Hence the result by definition of entropic structure.
{{qed}}
Theorem: Set of Endomorphisms on Entropic Structure is Closed in Induced Structure on Set of Self-Maps

Let $\struct {S, \odot}$ be a magma.
Let $\struct {S, \odot}$ be an entropic structure.
Let $S^S$ be the set of all mappings from $S$ to itself.
Let $\struct {S^S, \oplus}$ denote the algebraic structure on $S^S$ induced by $\odot$.
Let $T \subseteq S^S$ denote the set of endomorphisms on $\struct {S, \odot}$.
Then $\struct {T, \oplus_T}$ is closed in $\struct {S^S, \oplus}$.

Proof:
Recall the definition of algebraic structure on $S^S$ induced by $\odot$:
Let $f: S \to S$ and $g: S \to S$ be self-maps on $S$, and thus elements of $S^S$.
The pointwise operation on $S^S$ induced by $\odot$ is defined as:
:$\forall x \in S: \map {\paren {f \oplus g} } x = \map f x \odot \map g x$
Let $f, g \in T$ be arbitrary.
That is, let $f: S \to S$, $g: S \to S$ be endomorphisms on $\struct {S, \odot}$.
Let $x, y \in S$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map {\paren {f \oplus g} } {x \odot y}
      | r = \map f {x \odot y} \odot \map g {x \odot y}
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren {\map f x \odot \map f y} \odot \paren {\map g x \odot \map g y}
      | c = {{Defof|Endomorphism}}
}}
{{eqn | r = \paren {\map f x \odot \map g x} \odot \paren {\map f y \odot \map g y}
      | c = {{Defof|Entropic Structure}}
}}
{{eqn | r = \paren {\map {\paren {f \oplus g} } x} \odot \paren {\map {\paren {f \oplus g} } y}
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
demonstrating that $f \oplus g$ is a homomorphism from $S$ to itself.
Hence the result by definition of closed algebraic structure.
{{qed}}
Theorem: Replicative Function of x minus Floor of x is Replicative/Lemma

Let $x \in \R$.
Suppose $x - \floor x < \dfrac 1 n$.
Then:
:$\floor {x + \dfrac k n} = \dfrac {\floor  {n x} } n$
for any $0 \le k \le n - 1$.

Proof:
We have $n x < n \floor x + 1$.
By Number less than Integer iff Floor less than Integer:
:$\floor {n x} < n \floor x + 1$
Thus $\floor {n x} \le n \floor x$.
From definition of floor function:
:$n x \ge n \floor x$
By Number not less than Integer iff Floor not less than Integer:
:$\floor {n x} \ge n \floor x$
Therefore $\floor {n x} = n \floor x$ and thus $\floor x = \dfrac {\floor {n x} } n$.
Now we show $\floor {x + \dfrac k n} = \floor x$ for $0 \le k \le n - 1$.
We have:
:$\floor x \le \floor {x + \dfrac k n} \le \floor {x + \dfrac {n - 1} n}$
We also have:
:$x + \dfrac {n - 1} n < \floor x + \dfrac 1 n + \dfrac {n - 1} n = \floor x + 1$
By Number less than Integer iff Floor less than Integer:
:$\floor {x + \dfrac {n - 1} n} < \floor x + 1$
This gives:
:$\floor {x + \dfrac {n - 1} n} \le \floor x$
Combining the above:
:$\floor {x + \dfrac k n} = \floor x$
Therefore $\floor {x + \dfrac k n} = \floor x = \dfrac {\floor {n x} } n$.
{{qed}}
Category:Replicative Function of x minus Floor of x is Replicative
9vp67heeyu8gymdkimfhpg7mmtaeeo3