avewright/proofwiki-math huggingface dataset:
Theorem: Inverse of Circle Not Through Inversion Center

Let $\CC$ be a circle in the plane on center $O$.
Let $T : X \to Y$ be an inversive transformation with $\CC$ as the inversion circle. 
Then $O$ is the inversion center.
Let $K$ be an arbitrary circle distinct from $\CC$ and not through $O$.
Then the image under $T$ of all the points on $K$ lie on the same circle, distinct from both $K$ and $\CC$.

Proof:
:400px
Let the radius of $K$ be $k$.
Draw an arbitrary straight line from $O$ cutting $K$ at $A$ and $B$.  
Let $A'$ be the image of $A$ under $T$.
Let $B'$ be the image of $B$ under $T$.
There are two cases:  
:$(1): \quad$ The inversion circle $C$ may pass through straight line $OAB$ outside $K$
:$(2): \quad$ $C$ may cut $K$ and pass inside it.
The second possibility is illustrated using a dotted line.
The proof is the same for both.
Note:  the inversion circle is not shown, for clarity.
Let:
:$OA = a$
:$OB = b$
:$OA' = a'$
:$OB' = b'$
:$OM = m$
Let $t$ be the length of the tangent line to $K$ from $O$.
{{begin-eqn}}
{{eqn | l = a a'
      | r = b b' = r^2
      | c = Definition of $T$
}}
{{eqn | l = ab
      | r = t^2
      | c = Tangent Secant Theorem
}}
{{eqn | l = \dfrac {a'} b
      | r = \dfrac {b'} a = \dfrac {r^2} {t^2}
      | c = dividing by $t^2$
}}
{{end-eqn}}
Let the constant:
:$\dfrac {r^2} {t^2} = c^2$
Draw $A'Q \parallel BM$.
Let $OQ = q$.
Let $A'Q = p$.
By Equiangular Triangles are Similar:
:$\triangle OQA' \sim \triangle OMB$
:$\leadsto \dfrac q m = \dfrac {a'} b = c^2$
Also
:$\leadsto \dfrac p k = \dfrac {a'} b = c^2$
Substituting:
:$q = m c^2$
and
:$p = k c^2$
Since the {{RHS}} of both of these are constant, for all positions of $A$ and $B$:
:$Q$ is the same point on $OM$
The length $A'Q = p$ is constant.
$A'$ is always the same distance from $Q$.
Recall:
:$\dfrac {b'} a = c^2$
So {{mutatis}}:
:$B'Q = p$
$B'$ is also always the same distance from $Q$.
So $B'Q = A'Q$.
It follows that $A'$ and $B'$ both lie on the same circle.
{{qed}}
Theorem: Continuous Real-Valued Function on Compact Space is Bounded

Let $\struct {K, \tau}$ be a compact space.
Let $\R$ denote the real number line.
Let $f: S \to \R$ be a continuous real-valued function.
Then:
:$f$ is bounded.

Proof:
From Compact Space is Pseudocompact Space:
:$\struct {K, \tau}$ is pseudocompact
By definition of pseudocompact:
:$f$ is bounded.
{{qed}}
Theorem: Compact Space is Pseudocompact

Let $\struct {K, \tau}$ be a compact space.
Then $\struct {K, \tau}$ is a pseudocompact space

Proof:
Follows immediately from:
* Compact Space is Countably Compact
* Countably Compact Space is Pseudocompact
{{qed}}
Theorem: Ring of Bounded Continuous Functions is Ring of Continuous Functions for Pseudocompact Space

Let $\struct {K, \tau}$ be a pseudocompact space.
Let $\R$ denote the real number line.
Let $\struct {\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
Let $\struct {\map {C^*} {S, \R}, +, *}$ be the ring of bounded continuous real-valued functions from $S$.
Then:
:$\struct {\map {C^*} {S, \R}, +, *} = \struct {\map C {S, \R}, +, *}$

Proof:
Follows immediately from the definitions of:
* Definition:Pseudocompact Space
* Definition:Ring of Continuous Real-Valued Functions
* Definition:Ring of Bounded Continuous Real-Valued Functions
{{qed}}
Theorem: Lattice of Real-Valued Functions forms Distributive Lattice

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct {\R^S, \vee, \wedge, \le}$ be the lattice of real-valued functions from $S$ where:
:$\forall f, g \in \R^S : f \vee g : S \to \R$ is defined by:
::$\forall s \in S : \map {\paren{f \vee g}} s = \max \set{\map f s, \map g s}$
:$\forall f, g \in \R^S : f \wedge g : S \to \R$ is defined by:
::$\forall s \in S : \map {\paren{f \wedge g}} s = \min \set{\map f s, \map g s}$
:$\forall f, g \in \R^S : f \le g$ {{iff}}:
::$\forall x \in S : \map f x \le \map g x$
Then:
:$\struct {\R^S, \vee, \wedge, \le}$ is a distributive lattice.

Proof:
From Usual Ordering on Real Numbers is Total Ordering:
:$\struct {\R, \le}$ is totally ordered
where $\le$ denotes the usual ordering on $\R$.
From Totally Ordered Set is Lattice
:$\struct{\R, \le}$ is a lattice.
By definition of join:
:$\forall x, y \in \R : x \vee y = \sup \set {x, y}$
where $x \vee y$ denotes the join of $x$ and $y$ in $\struct {\R, \le}$.
From Max Operation Yields Supremum of Parameters:
:$\forall x, y \in \R : \map \max {x, y} = \sup \set {x, y} = x \vee y$
By definition of meet:
:$\forall x, y \in \R : x \wedge y = \inf \set {x, y}$
where $x \wedge y$ denotes the meet of $x$ and $y$ in $\struct {\R, \le}$.
From Min Operation Yields Infimum of Parameters:
:$\forall x, y \in \R : \map \min {x, y} = \inf \set {x, y} = x \wedge y$
From Structure Induced by Lattice Operations is Lattice:
:$\struct {\R^S, \vee, \wedge, \le}$ is a lattice.
From Max and Min Operations are Distributive over Each Other:
:$\struct {\R, \vee, \wedge, \le}$ is a distributive lattice.
From Structure Induced by Distributive Operation is Distributive:
:$\struct {\R^S, \vee, \wedge, \le}$ is a distributive lattice.
{{qed}}
Category:Distributive Lattices
Category:Real-Valued Functions
afl8khxgvj5inkra39bv672ykgaabh2
Theorem: Structure Induced by Idempotent Operation is Idempotent

Let $\struct {T, \circ}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus}$ be the structure on $T^S$ induced by $\circ$.
Let $\circ$ be an idempotent operation.
Then the pointwise operation $\oplus$ induced on $T^S$ by $\circ$ is also idempotent.

Proof:
Let $f \in T^S$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {f \oplus f} } x
      | r = \map f x \circ \map f x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x 
      | c = $\circ$ is idempotent operation
}}
{{end-eqn}}
From Equality of Mappings:
:$f \oplus f = f$
Since $f$ was arbitrary:
:$\forall f \in T^S : f \oplus f = f$
Hence $\oplus$ is idempotent by definition.
{{qed}}
Category:Pointwise Operations
Category:Idempotence
3v6oyf3d5xz4xjc8c6athb8yiaw3vjv
Theorem: Structure Induced by Lattice Operations is Lattice

Let $\struct {L, \vee, \wedge, \preceq}$ be a lattice.
Let $S$ be a set.
Let $\struct {L^S, \veebar, \barwedge}$ be the structure on $T^S$ induced by $\vee$ and $\wedge$.
Let $\precsim$ be the ordering on $S$ defined by:
:$\forall f, g \in L^S: f \precsim g$ {{iff}} $f \veebar g = g$
as on Semilattice Induces Ordering.
Then $\struct {L^S, \veebar, \barwedge, \precsim}$ is a lattice.

Proof:
=== $\struct {L^S, \veebar}$ and $\struct {L^S, \barwedge}$ are Semilattices ===
By definition of lattice:
:$\struct {L, \vee}$ and $\struct {L, \wedge}$ are semilattices.
From Structure Induced by Semilattice Operation is Semilattice:
:$\struct {L^S, \veebar}$ and $\struct {L^S, \veebar}$ are semilattices.
{{qed|lemma}}
Theorem: Structure Induced by Absorbing Operations is Absorbing

Let $\struct {T, \circ, *}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus, \otimes}$ be the structure on $T^S$ induced by $\circ$ and $*$.
Let $\circ$ and $*$ satisfy the absorption law:
:$\forall a, b \in S: a \circ \paren {a * b} = a$
Then the pointwise operations $\oplus$ and $\otimes$ on $T^S$ also satisfy the absorption law:
:$\forall f, g \in T^S: f \oplus \paren {f \otimes g} = f$

Proof:
Let $f, g \in T^S$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {f \oplus \paren {f \otimes g} } } x
      | r = \map f x \circ \map {\paren {f \otimes g} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x \circ \paren {\map f x * \map g x}
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x 
      | c = $\circ$ absorbs $*$
}}
{{end-eqn}}
From Equality of Mappings:
:$f \oplus \paren {f \otimes g} = f$
Since $f, g$ were arbitrary:
:$\forall f, g \in T^S : f \oplus \paren {f \otimes g} = f$
Hence $\oplus$ absorbs $\otimes$ by definition.
{{qed}}
Category:Absorption Laws
Category:Pointwise Operations
rh5xo8g4w2pq2djefwedu38phuefl8m
Theorem: Structure Induced by Semilattice Operation is Semilattice

Let $\struct {T, \circ}$ be a semilattice.
Let $S$ be a set.
Let $\struct {T^S, \oplus}$ be the structure on $T^S$ induced by $\circ$.
Then $\struct {T^S, \oplus}$ is a semilattice.

Proof:
Taking the semilattice axioms in turn:
Theorem: Perpendicular from Point to Straight Line in Plane is Unique

Let $BC$ be a straight line in the plane.
Let $AM$ be perpendicular to $BC$ at $M$.
Let $P$ be an arbitrary point on the same side of $BC$ as $A$ is, but not on $AM$.
Then $PM$ cannot be perpendicular to $BC$.

Proof:
:250px
{{WLOG}} let $M$ bisect $BC$.
{{AimForCont}} $PM \perp BC$.
By definition $PM$ is a perpendicular bisector of $BC$ at $M$.
Then by definition of perpendicular bisector:
:$PC = PB$
Find $P'$ on $AM$ such that $P'C = PC$.
Since $AM$ is also a perpendicular bisector of $BC$:
:$P'B = P'C$
:$\leadsto PB = PC = P'C = P'B$
{{:Euclid:Proposition/I/7}}
This is a contradiction.
Therefore, no such $P$ exists.
All points equidistant from $B$ and $C$, on the same side of $BC$ as $A$, lie on $AM$.
{{qed}}
Theorem: Products of Homeomorphic Spaces are Homeomorphic

Let:
:$\sequence {T_i}_{i \mathop \in I}$
:$\sequence {T'_i}_{i \mathop \in I}$
be indexed families of topological spaces, with indexing set $I$.
Let:
:$\sequence {\phi_i}_{i \mathop \in I}$
be an indexed family of homeomorphisms $\phi_i$ from $T_i$ to $T'_i$.
Define:
:$\ds T = \prod_{i \mathop \in I} T_i$
:$\ds T' = \prod_{i \mathop \in I} T'_i$
where $\ds \prod_{i \mathop \in I} T_i$ denotes the product space.
Then, the mapping $\phi : T \to T'$ defined as:
:$\map \phi x = \sequence {\map {\phi_i \circ \pr_i} x}_{i \mathop \in I}$
is a homeomorphism from $T$ to $T'$.

Proof:
We have that:
:$\map {\phi^{-1}} x = \sequence {\map {\phi_i^{-1} \circ \pr_i} x}_{i \mathop \in I}$
For:
{{begin-eqn}}
{{eqn | l = \map \phi {\map {\phi^{-1} } x}
      | r = \sequence {\map {\phi_i \circ \pr_i} {\sequence {\map {\phi_i^{-1} \circ \pr_i} x}_{i \mathop \in I} } }_{i \mathop \in I}
}}
{{eqn | r = \sequence {\map {\phi_i \circ \phi_i^{-1} \circ \pr_i} x }_{i \mathop \in I}
}}
{{eqn | r = \sequence {\map {\pr_i} x}_{i \mathop \in I}
      | c = {{Defof|Inverse Mapping}}
}}
{{eqn | r = x
}}
{{eqn | l = \map {\phi^{-1} } {\map \phi x}
      | r = \sequence {\map {\phi_i^{-1} \circ \pr_i} {\sequence {\map {\phi_i \circ \pr_i} x}_{i \mathop \in I} } }_{i \mathop \in I}
}}
{{eqn | r = \sequence {\map {\phi_i^{-1} \circ \phi_i \circ \pr_i} x}_{i \mathop \in I}
}}
{{eqn | r = \sequence {\map {\pr_i} x}_{i \mathop \in I}
      | c = {{Defof|Inverse Mapping}}
}}
{{eqn | r = x
}}
{{end-eqn}}
It follows that $\phi$ is a bijection.
Additionally, by:
* Projection from Project Topology is Continuous
* Composite of Continuous Mappings is Continuous
* Continuous Mapping to Product Space
it follows that both $\phi$ and $\phi^{-1}$ are continuous.
Therefore, $\phi$ is a homeomorphism by definition.
{{qed}}
Category:Homeomorphisms (Topological Spaces)
Category:Product Topology
cw0cxdv8itunwkypzh25jx8blmr8j9l
Theorem: Rotation in Euclidean Space is Conformal

Let $f$ be an rotation in Euclidean space.
Then $f$ is a conformal transformation.

Proof:
{{ProofWanted}}
Category:Geometric Rotations
Category:Conformal Transformations
s2rtr95rl73qb00l4o4qczb1lf2yn99
Theorem: Lattice and Ring of Real-Valued Functions forms Ordered Ring

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct {\R^S, +, \times}$ be the ring of real-valued functions from $S$ to $\R$.
Let $\struct {\R^S, \vee, \wedge, \le}$ be the lattice of real-valued functions from $S$ to $\R$.
Then:
:$\struct {\R^S, +, \times, \le}$ is an ordered ring

Proof:
From Structure Induced by Group Operation is Group:
:the zero of $\struct {\R^S, +, \times}$ is the constant mapping $0_{R^S} : S \to R$ defined by:
::$\forall s \in S : \map {0_{R^S}} s = 0_R$
It needs to be shown that the order $\le$ on the lattice of real-valued functions satisies the ring compatible ordering axioms:
{{begin-axiom}}
{{axiom | n = \text {OR} 1
        | lc= $\le$ is compatible with $+$:
        | q = \forall f, g, h \in \R^S
        | ml= f \le g
        | mo= \implies
        | mr= \paren {f + h} \le \paren {g + h}
}}
{{axiom | n = \text {OR} 2
        | lc= Product of Positive Elements is Positive
        | q = \forall f, g \in \R^S
        | ml= 0_{\R^S} \le f, 0_{\R^S} \le g
        | mo= \implies
        | mr= 0_{\R^S} \le f g
}}
{{end-axiom}}
Theorem: Eccentricity of Parabola equals 1

The parabola has eccentricity equal to $1$.

Proof:
Let $K$ be a '''conic section'''.
From the focus-directrix property of a conic section, $K$ is the locus of points $b$ such that the distance $p$ from $b$ to $D$ and the distance $q$ from $b$ to $F$ are related by the condition:
:$(1): \quad q = \epsilon p$
where $\epsilon$ denotes the eccentricity.
Now let $K$ be a parabola.
From the focus-directrix property of the parabola, $K$ is the locus of points $P$ such that the distance $p$ from $P$ to $D$ equals the distance $q$ from $P$ to $F$:
:$p = q$
This is an instance of $(1)$ where $\epsilon = 1$.
Hence the result.
{{qed}}
Theorem: Value of Discriminant of Conic Section

Let $K$ be a conic section embedded in a Cartesian plane with the general equation:
:$a x^2 + 2 h x y + b y^2 + 2 g x + 2 f y + c = 0$
where $a, b, c, f, g, h \in \R$.
The value of the discriminant of $K$ is:
:$\Delta = a b c + 2 f g h - a f^2 - b g^2 - c h^2$

Proof:
By definition, the discriminant of $K$ is:
{{begin-eqn}}
{{eqn | l = \Delta
      | r = \begin {vmatrix} a & h & g \\ h & b & f \\ g & f & c \end {vmatrix}
      | c = {{Defof|Discriminant of Conic Section}}
}}
{{eqn | r = a \paren {b c - f^2} - h \paren {h c - g f} + g \paren {h f - g b}
      | c = Laplace Expansion Theorem for Determinants
}}
{{eqn | r = a b c - a f^2 - h^2 c + h g f + h g f - g^2 b
      | c = Multiplication Distributes over Addition
}}
{{eqn | r = a b c + 2 f g h - a f^2 - b g^2 - c h^2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Lattice of Continuous Functions is Sublattice of All Real-Valued Functions

Let $\struct {S, \tau }$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct {\R^S, \vee, \wedge, \le}$ be the lattice of real-valued functions from $S$.
Let $\struct{\map C {S, R}, \vee, \wedge, \le}$ be the lattice of continuous real-valued functions from $S$.
Then:
:$\struct{\map C {S, R}, \vee, \wedge, \le}$ is a sublattice of $\struct {\R^S, \vee, \wedge, \le}$

Proof:
To show that $\struct{\map C {S, R}, \vee, \wedge, \le}$ is a sublattice of $\struct {\R^S, \vee, \wedge, \le}$ it is sufficient to show that $\map C {S, R}$ is closed under $\vee$ and $\wedge$.
From Maximum Rule for Continuous Real-Valued Functions:
:$\map C {S, R}$ is closed under $\vee$
From Minimum Rule for Continuous Real-Valued Functions:
:$\map C {S, R}$ is closed under $\wedge$
{{qed}}
Category:Lattices of Continuous Real-Valued Functions
754sy3nuljq2i48p9t70zesg2tr36zk
Theorem: Classification of Conic Sections by Coefficients of General Equation

Let $K$ be a conic section embedded in a Cartesian plane with the general equation:
:$a x^2 + 2 h x y + b y^2 + 2 g x + 2 f y + c = 0$
where $a, b, c, f, g, h \in \R$.
Let $\Delta$ denote the discriminant of $K$:
:$\Delta = \begin {vmatrix} a & h & g \\ h & b & f \\ g & f & c \end {vmatrix}$
If $\Delta \ne 0$, then $K$ is an ellipse, a parabola or a hyperbola, according to:
{{begin-eqn}}
{{eqn | l = h^2 - a b
      | o = <
      | r = 0:
      | c = $K$ is an ellipse
}}
{{eqn | l = h^2 - a b
      | r = 0:
      | c = $K$ is a parabola
}}
{{eqn | l = h^2 - a b
      | o = >
      | r = 0:
      | c = $K$ is a hyperbola
}}
{{end-eqn}}
If $\Delta = 0$, then $K$ is a degenerate conic:
{{begin-eqn}}
{{eqn | l = h^2 - a b
      | o = <
      | r = 0:
      | c = $K$ is a point
}}
{{eqn | l = h^2 - a b
      | r = 0:
      | c = $K$ is a pair of parallel lines or coincident straight lines, or an imaginary locus
}}
{{eqn | l = h^2 - a b
      | o = >
      | r = 0:
      | c = $K$ is a pair of intersecting straight lines
}}
{{end-eqn}}

Proof:
{{ProofWanted|a satisfying job for a rainy day}}
Theorem: Lattice of Bounded Continuous Functions is Sublattice of Continuous Real-Valued Functions

Let $\struct {S, \tau }$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct{\map C {S, R}, \vee, \wedge, \le}$ be the lattice of continuous real-valued functions from $S$.
Let $\struct{\map {C^*} {S, R}, \vee, \wedge, \le}$ be the lattice of bounded continuous real-valued functions from $S$.
Then:
:$\struct{\map {C^*} {S, R}, \vee, \wedge, \le}$ is a sublattice of $\struct{\map C {S, R}, \vee, \wedge, \le}$

Proof:
To show that $\struct{\map {C^*} {S, R}, \vee, \wedge, \le}$ is a sublattice of $\struct {\map C {S, R}, \vee, \wedge, \le}$ it is sufficient to show that $\map {C^*} {S, R}$ is closed under $\vee$ and $\wedge$.
From Maximum Rule for Bounded Continuous Real-Valued Functions:
:$\map {C^*} {S, R}$ is closed under $\vee$
From Minimum Rule for Bounded Continuous Real-Valued Functions:
:$\map {C^*} {S, R}$ is closed under $\wedge$
{{qed}}
Category:Lattices of Bounded Continuous Real-Valued Functions
ctvvl2cjv60wie8xerd39xm9jy06bqw
Theorem: Projection of Conic Section is Conic Section

Let $K$ be a conic section.
Let $K'$ be a projection of $K$.
Then $K'$ is also a conic section.

Proof:
{{ProofWanted|needs background work completed}}
Theorem: Real Number Line less Zero is Disconnected Space

Let $S := \R \setminus \set 0$ be the real number line with $0$ excluded.
Let $\struct {S, \tau_d}$ be $S$ with the usual (Euclidean) topology.
Then $\struct {S, \tau_d}$ is disconnected.

Proof:
We note that:
:$S = \openint \gets 0 \cup \openint 0 \to$
:$\openint \gets 0 \cap \openint 0 \to = \O$
Hence we have partitioned $S$ into $2$ disjoint open sets whose union is $S$.
Hence by definition $S$ is not connected.
Hence the result by definition of disconnected space.
{{qed}}
Theorem: Positive Real Number has Simple Continued Fraction Expansion

Let $x \in \R_{>0}$ be a (strictly) positive real number.
Then $x$ can be expressed as a simple continued fraction.

Proof:
We have that $x$ is either rational or irrational.
;$x$ rational
Let $x$ be rational.
Then from Rational Number can be Expressed as Simple Finite Continued Fraction, $x$ has a simple continued fraction expansion.
;$x$ irrational
Let $x$ be irrational.
The result follows from Correspondence between Irrational Numbers and Simple Infinite Continued Fractions.
{{qed}}
Theorem: Parallelogram with One Right Angle is Rectangle

Let $\Box ABCD$ be a parallelogram.
Let one angle of $\Box ABCD$ be a right angle.
Then $\Box ABCD$ is a rectangle.

Proof:
{{WLOG}}, let $\angle ABC$ be a right angle.
Let $\angle CDA$ be opposite $\angle ABC$.
By Opposite Sides and Angles of Parallelogram are Equal:
:$\angle CDA = \angle ABC$
By Sum of Internal Angles of Polygon:
: the sum of the angles of $\Box ABCD$ is four right angles.
Hence:
$\angle DAB + \angle BCD$ together equal two right angles.
By Opposite Sides and Angles of Parallelogram are Equal:
:$\angle DAB = \angle BCD$
Hence, all four angles of $\Box ABCD$ are right angles.
By Opposite Sides and Angles of Parallelogram are Equal:
:$AB = CD$
:$AD = BC$
$\leadsto$
:$\Box ABCD$ is a rectangle.
The result follows.
{{qed}}
Category:Parallelograms
Category:Rectangles
4v3w1tm6ngqyuog3jdwciaaq92s0mp3
Theorem: Structure Induced by Left Distributive Operation is Left Distributive

Let $\struct {T, +, \times}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus, \otimes}$ be the structure on $T^S$ induced by $+$ and $\times$.
Let $\times$ be left distributive over $+$:
:$\forall a, b, c \in S: a \times \paren {b + c} = \paren{a \times b} + \paren{a \times c}$
Then the pointwise operation $\otimes$ is left distributive over the pointwise operation $\oplus$ on $T^S$:
:$\forall f, g, h \in T^S: f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$

Proof:
Let $f, g, h \in T^S$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren{f \otimes \paren {g \oplus h} } } x
      | r = \map f x \times \map {\paren{g \otimes h} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map f x \times \paren{ \map g x + \map h x}
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren{\map f x \times \map g x} + \paren{\map f x \times \map h x}
      | c = {{defof|Left Distributive Operation}}
}}
{{eqn | r = \map {\paren{f \otimes g} } x + \map {\paren{f \otimes h} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map {\paren{\paren{f \otimes g} \oplus \paren{f \otimes h} } } x
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
From Equality of Mappings:
:$f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$
Since $f, g, h$ were arbitrary:
:$\forall f, g, h \in T^S: f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$
Hence $\otimes$ is left distributive over $\oplus$ by definition.
{{qed}}
Category:Pointwise Operations
Category:Distributive Operations
d1mh0o3jbtheofyx2ya8g2lvzfszu5o
Theorem: Structure Induced by Right Distributive Operation is Right Distributive

Let $\struct {T, +, \times}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus, \otimes}$ be the structure on $T^S$ induced by $+$ and $\times$.
Let $\times$ be right distributive over $+$:
:$\forall a, b, c \in S: \paren {b + c} \times a= \paren{b \times a} + \paren{c \times a}$
Then the pointwise operation $\otimes$ is left distributive over the pointwise operation $\oplus$ on $T^S$:
:$\forall f, g, h \in T^S: \paren {g \oplus h} \otimes f = \paren{g \otimes f} \oplus \paren{h \otimes f}$

Proof:
Let $f, g, h \in T^S$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren{\paren {g \oplus h} \otimes f} } x
      | r = \map {\paren{g \otimes h} } x \times \map f x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren{ \map g x + \map h x} \times \map f x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \paren{\map g x \times \map f x} + \paren{\map h x \times \map f x}
      | c = {{defof|Right Distributive Operation}}
}}
{{eqn | r = \map {\paren{g \otimes f } } x + \map {\paren{h \otimes f} } x
      | c = {{Defof|Pointwise Operation}}
}}
{{eqn | r = \map {\paren{\paren{g \otimes f} \oplus \paren{h \otimes f} } } x
      | c = {{Defof|Pointwise Operation}}
}}
{{end-eqn}}
From Equality of Mappings:
:$\paren {g \oplus h} \otimes f = \paren{g \otimes f} \oplus \paren{h \otimes f}$
Since $f, g, h$ were arbitrary:
:$\forall f, g, h \in T^S: \paren {g \oplus h} \otimes f = \paren{g \otimes f} \oplus \paren{h \otimes f}$
Hence $\otimes$ is right distributive over $\oplus$ by definition.
{{qed}}
Category:Pointwise Operations
Category:Distributive Operations
5v61l8b1sjj6vj17o37o8u3s4qd02pl
Theorem: Structure Induced by Distributive Operation is Distributive

Let $\struct {T, +, \times}$ be an algebraic structure, and let $S$ be a set.
Let $\struct {T^S, \oplus, \otimes}$ be the structure on $T^S$ induced by $+$ and $\times$.
Let $\times$ be distributive over $+$:
:$\forall a, b, c \in S$: 
::$a \times \paren {b + c} = \paren{a \times b} + \paren{a \times c}$
:and:
::$\paren {b + c} \times a= \paren{b \times a} + \paren{c \times a}$
Then the pointwise operation $\otimes$ is distributive over the pointwise operation $\oplus$ on $T^S$:
:$\forall f, g, h \in T^S$:
::$f \otimes \paren {g \oplus h} = \paren{f \otimes g} \oplus \paren{f \otimes h}$
:and:
::$\paren {g \oplus h} \otimes f = \paren{g \otimes f} \oplus \paren{h \otimes f}$

Proof:
By definition of distributive operation:
:$\times$ is left distributive over $+$
and
:$\times$ is right distributive over $+$
From Structure Induced by Left Distributive Operation is Left Distributive:
:$\otimes$ is left distributive over $\oplus$
From Structure Induced by Right Distributive Operation is Right Distributive:
:$\otimes$ is right distributive over $\oplus$
It follws that $\otimes$ is distributive over $\oplus$ by definition.
{{qed}}
Category:Pointwise Operations
Category:Distributive Operations
nnbsh5vhr84wq9gv0t7cy9pwihnx5wk