nyuuzyou/wikis huggingface dataset:
Extension of Bounded Linear Transformation from Closed Subspace of Hilbert Space to Whole Space

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $\struct {\HH_1, \innerprod \cdot \cdot_1}$ and $\struct {\HH_2, \innerprod \cdot \cdot_2}$ be Hilbert spaces over $\GF$.
Let $\KK_1$ and $\KK_2$ be closed linear subspaces of $\HH_1$ and $\HH_2$ respectively.
Let $T_1 : \KK_1 \to \KK_2$ be a bounded linear transformation.
Let $\KK_1^\bot$ of $\KK_2^\bot$ be the orthocomplements of $\KK_1$ and $\KK_2$ respectively.
Let $T_2 : \KK_1^\bot \to \KK_2^\bot$ be a bounded linear transformation.
Define $T : \HH_1 \to \HH_2$ by:
:$\map T {u + v} = T_1 u + T_2 v$
for each $u \in \KK_1$ and $v \in \KK_1^\bot$. 
Then $T$ is a bounded linear transformation extending $T_1$. 
== Proof ==
We first show that $T$ is well-defined. 
Let $u_1, u_2 \in \KK_1$ and $v_1, v_2 \in \KK_2$.
From Direct Sum of Subspace and Orthocomplement, we have $\KK_1 \oplus \KK_1^\bot = \HH_1$ as an internal direct sum.
Hence $\KK_1 \cap \KK_1^\bot = \set { {\mathbf 0}_\HH}$, and if $u_1 + v_1 = u_2 + v_2$, then $u_1 = u_2$ and $v_1 = v_2$.
Hence $T$ is well-defined.
We show that $T$ is linear.
Let $x, y \in \HH$ and $\lambda \in \GF$. 
Since $\KK_1 \oplus \KK_1^\bot = \HH_1$, there exists $u_1, u_2 \in \KK_1$ and $v_1, v_2 \in \KK_1^\bot$ such that:
:$x = u_1 + v_1$
and:
:$y = u_2 + v_2$
We then have:
:$x + \lambda y = \paren {u_1 + \lambda u_2} + \paren {v_1 + \lambda v_2}$
where $u_1 + \lambda u_2 \in \KK_1$ and $v_1 + \lambda v_2 \in \KK_1^\bot$.
Hence:
So $T$ is linear.
We show that $T$ is bounded.
Let $x \in \HH$ and take $u \in \KK_1$, $v \in \KK_1^\bot$ such that $x = u + v$.
We then have:
We conclude that:
:$\norm {T x}_2 \le \sqrt {\max \set {M_1, M_2} } \norm x_1$ 
for each $x \in \HH$.
So $T$ is a bounded transformation.
Finally, for $x \in \KK_1$ we have:
:$T x = \map T {x + {\mathbf 0}_\HH} = T_1 x + \map {T_2} { {\mathbf 0}_\HH} = T_1 x$
since $T_2$ is linear.
Hence $T$ extends $T_1$.
Category:Bounded Linear Transformations
Category:Hilbert Spaces
Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous

== Theorem ==
Let $X$ be a locally compact Hausdorff space.
Let $X^\ast = X \cup \set p$ be the Alexandroff extension of $X$.
Let $f : X \to \C$ be a continuous complex-valued function vanishing at infinity.
Define $f^\ast : X^\ast \to \C$ by taking:
:$\map {f^\ast} x = \begin{cases}\map f x & x \in X \\ 0 & x = p\end{cases}$
for each $x \in X^\ast$. 
Then $f^\ast$ is continuous. 
=== Corollary ===
== Proof ==
Since $f$ is continuous at each $x \in X$, we have:
:for each $x \in X$:
::for every open neighborhood $U_2$ of $\map f x \in \C$, there exists an open neighborhood $U_1$ of $x \in X$ such that $f \sqbrk {U_1} \subseteq U_2$.
From the definition of the topology on $X^\ast$:
:every open set in $X$ is open in $X^\ast$.
Hence the $U_1$ given above remains an open neighborhood of $x$ in $X^\ast$.
Since $\map {f^\ast} x = \map f x$ for $x \in X$, $f^\ast$ remains continuous at each $x \in X$. 
We therefore only need to concern ourselves with continuity at $p$.
Let $U_2$ be an open neighborhood of $0 \in \C$.
Then there exists $\epsilon > 0$ such that $\set {z \in \C : \cmod z < \epsilon} \subseteq U_2$. 
From the definition of a complex-valued function vanishing at infinity, there exists a compact set $K \subseteq X$ such that:
:$\cmod {\map f x} < \epsilon$ for $x \in X \setminus K$. 
We also have $\cmod {\map {f^\ast} p} = 0 < \epsilon$, so we have:
:$\cmod {\map {f^\ast} x} < \epsilon$ for $x \in \set p \cup \paren {X \setminus K}$.
From the definition of the topology on $X^\ast$:
:$\set p \cup \paren {X \setminus K}$ is open in $X^\ast$.
Hence setting $U_1 = \set p \cup \paren {X \setminus K}$, we have:
:${f^\ast} \sqbrk {U_1} \subseteq \set {z \in \C : \cmod z < \epsilon} \subseteq U_2$
with $p \in U_1$.
So $f^\ast$ is continuous at $p$.
Hence $f^\ast$ is continuous.
Category:Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous
Category:Alexandroff Extensions
Category:Complex-Valued Functions Vanishing at Infinity
Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous/Corollary

== Theorem ==
Let $X$ be a locally compact Hausdorff space.
Let $f : X \to \C$ be a continuous complex-valued function vanishing at infinity.
Then $f \sqbrk X \cup \set 0$ is compact.
== Proof ==
Let $X^\ast = X \cup \set p$ be the Alexandroff extension of $X$.
From Alexandroff Extension is Compact, $X^\ast$ is compact.
Define $f^\ast : X^\ast \to \C$ by taking:
:$\map {f^\ast} x = \begin{cases}\map f x & x \in X \\ 0 & x = p\end{cases}$
for each $x \in X^\ast$. 
From Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous, $f^\ast$ is continuous.
From Continuous Image of Compact Space is Compact, $f^\ast \sqbrk {X^\ast}$ is compact.
We have:
Hence $f \sqbrk X \cup \set 0$ is compact.
Category:Extension of Continuous Complex-Valued Function Vanishing at Infinity to Alexandroff Extension is Continuous
Extension of Continuous Mapping is Continuous

== Theorem ==
Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $T_H = \struct{H, \tau_H}$ be a topological subspace of $T_2$ where $H \subseteq S_2$.
Let $f: S_1 \to H$ be a $\tuple { \tau_1 , \tau_H}$-continuous mapping.
Define a mapping $g: S_1 \to S_2$ by:
:$\forall x \in S_1 : \map g x = \map f x$
Then $g$ is $\tuple { \tau_1 , \tau_2}$-continuous.
== Proof ==
Let $i_H$ be the inclusion mapping of $H$ in $S_2$.
Then:
:$g = i_H \circ f$
From Continuity of Composite with Inclusion: Inclusion on Mapping, it follows that $f$ is $\tuple { \tau_1 , \tau_H}$-continuous mapping $i_H \circ f = g$ is $\tuple { \tau_1 , \tau_2}$-continuous.
Since $f$ is continuous by assumption, $g$ is continuous.
== Sources ==
* : $\S 3$: New Spaces From Old: Subspaces
Extension of Contraction of Extension of Ideal is Extension

== Theorem ==
Let $A$ and $B$ be commutative rings with unity.
Let $f : A \to B$ be a ring homomorphism.
Let $\mathfrak a$ be an ideal of $A$.
Let ${\mathfrak a}^e$ be the extension of $\mathfrak a$ by $f$.
Let ${\mathfrak a}^{ec}$ be the contraction of ${\mathfrak a}^e$ by $f$.
Let ${\mathfrak a}^{ece}$ be the extension of ${\mathfrak a}^{ec}$ by $f$.
Then:
:${\mathfrak a}^e = {\mathfrak a}^{ece}$
== Proof ==
Since $\mathfrak a \subseteq {\mathfrak a}^{ec}$ by Ideal is Contained in Contraction of Extension:
Category:Ideal Theory
Category:Commutative Algebra
Category:Ring Theory
Extension of Contradictory Branch is Contradictory

== Theorem ==
Let $T$ be a propositional tableau.
Let $\Gamma$ be a contradictory branch of $T$.
Let $\Gamma'$ be an extension of $\Gamma$.
Then $\Gamma'$ is also contradictory.
== Proof ==
Since $\Gamma$ is contradictory, there is some WFF $\mathbf A$ such that both $\mathbf A$ and $\neg \mathbf A$ occur along $\Gamma$.
Since $\Gamma'$ is an extension of $\Gamma$, $\mathbf A$ and $\neg \mathbf A$ also occur along $\Gamma'$.
Hence $\Gamma'$ is contradictory.
Category:Propositional Tableaux
Extension of Directed Suprema Preserving Mapping to Complete Lattice Preserves Directed Suprema

== Theorem ==
Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be ordered sets.
Let $L_3 = \struct {S_3, \preceq_3}$ be a complete lattice.
Suppose that
:$L_2$ is directed suprema inheriting ordered subset of $L_3$.
Let $f:S_1 \to S_2$ be a mapping such that
:$f$ preserves directed suprema.
Then
$f:S_1 \to S_3$ preserves directed suprema.
== Proof ==
By definition of ordered subset:
:$S_2 \subseteq S_3$
Then define $g = f: S_1 \to S_3$
Let $X$ be a directed subset of $S_1$ such that
:$X$ admits a supremum in $L_1$.
Thus by definition of complete lattice:
:$g \sqbrk X$ admits a supremum in $L_3$.
By definition of mapping preserves directed suprema:
:$f \sqbrk X$ admits a supremum in $L_2$ and $\map {\sup_{L_2} } {f \sqbrk X} = \map f {\sup_{L_1} X}$
By Directed Suprema Preserving Mapping is Increasing:
:$f$ is an increasing mapping.
By Image of Directed Subset under Increasing Mapping is Directed:
:$f \sqbrk X$ is directed.
Thus by definition of directed suprema inheriting:
:$\map {\inf_{L_3} } {g \sqbrk X} = \map g {\inf_{L_1} X}$
== Sources ==
* 
Category:Order Theory
Category:Complete Lattices
Extension of Extension of Mapping is Extension

== Theorem ==
Let $A, B, C, S$ be sets such that $A \subseteq B \subseteq C$.
Let $f: A \to S$, $g: B \to S$ and $h: C \to S$ be mappings such that:
:$g$ is an extension of $f$ to $B$
:$h$ is an extension of $g$ to $C$.
Then $h$ is an extension of $f$ to $C$.
== Proof ==
By definition of extension:
:$\forall x \in A: \map f x = \map g x$
and:
:$\forall x \in B: \map g x = \map h x$
and so:
:$\forall x \in A: \map g x = \map h x$
from which it follows that:
:$\forall x \in A: \map f x = \map h x$
== Sources ==
* : Chapter $1$: Theory of Sets: $\S 9$: Inverse Functions, Extensions, and Restrictions: Exercise $3$
Category:Restrictions
Extension of Half-Range Fourier Cosine Function to Symmetric Range

== Theorem ==
Let $\map f x$ be a real function defined on the interval $\openint 0 \lambda$.
Let $\map f x$ be represented by the half-range Fourier cosine series $\map S x$:
:$\map f x \sim \map S x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty a_n \cos \frac {n \pi x} \lambda$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \cos \frac {n \pi x} \lambda \rd x$
Then $\map S x$ also represents the extension to the even function $g: \openint {-\lambda} \lambda \to \R$ of $f$, defined as:
:$\forall x \in \openint {-\lambda} \lambda: \map g x = \begin {cases} \map f x & : x > 0 \\ \map f {-x} & : x < 0 \\ \ds \lim_{x \mathop \to 0} \map g x & : x = 0 \end {cases}$
== Proof ==
It is apparent by inspection that:
:$(1): \quad g$ is an extension of $f$
:$(2): \quad g$ is an even function.
Let $\map T x$ be the Fourier series representing $g$:
:$\map g x \sim \map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos \frac {n \pi x} \lambda + b_n \sin \frac {n \pi x} \lambda}$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
:$b_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
From Fourier Sine Coefficients for Even Function over Symmetric Range:
:$\forall n \in \Z_{> 0}: b_n = 0$
and from Fourier Cosine Coefficients for Even Function over Symmetric Range:
:$\forall n \in \Z_{>0}: a_n = \ds \frac 2 \lambda \int_0^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
But on $\openint 0 \lambda$, by definition:
:$\forall x \in \openint 0 \lambda: \map g x = \map f x$
Hence:
:$\map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren a_n \cos \frac {n \pi x} \lambda$
where:
:$a_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \cos \frac {n \pi x} \lambda \rd x$
That is, $\map T x$ is the same as $\map S x$.
Hence the result.
Category:Half-Range Fourier Series
Extension of Half-Range Fourier Sine Function to Symmetric Range

== Theorem ==
Let $\map f x$ be a real function defined on the interval $\openint 0 \lambda$.
Let $\map f x$ be represented by the half-range Fourier sine series $\map S x$:
:$\map f x \sim \map S x = \ds \sum_{n \mathop = 1}^\infty b_n \sin \frac {n \pi x} \lambda$
where for all $n \in \Z_{> 0}$:
:$b_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \sin \frac {n \pi x} \lambda \rd x$
Then $\map S x$ also represents the extension $g: \openint {-\lambda} \lambda \to \R$ of $f$, defined as:
:$\forall x \in \openint {-\lambda} \lambda: \map g x = \begin {cases} \map f x & : x > 0 \\ -\map f {-x} & : x < 0 \\ 0 & : x = 0 \end {cases}$
== Proof ==
It is apparent by inspection that:
:$(1): \quad g$ is an extension of $f$
:$(2): \quad g$ is an odd function.
Let $\map T x$ be the Fourier series representing $g$:
:$\map g x \sim \map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos \frac {n \pi x} \lambda + b_n \sin \frac {n \pi x} \lambda}$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
:$b_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
From Fourier Cosine Coefficients for Odd Function over Symmetric Range:
:$\forall n \in \Z_{\ge 0}: a_n = 0$
and from Fourier Sine Coefficients for Odd Function over Symmetric Range:
:$\forall n \in \Z_{>0}: b_n = \ds \frac 2 \lambda \int_0^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
But on $\openint 0 \lambda$, by definition:
:$\forall x \in \openint 0 \lambda: \map g x = \map f x$
Hence:
:$\map T x = \ds \sum_{n \mathop = 1}^\infty \paren b_n \sin \frac {n \pi x} \lambda$
where:
:$b_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \sin \frac {n \pi x} \lambda \rd x$
That is, $\map T x$ is the same as $\map S x$.
Hence the result.
Category:Half-Range Fourier Series
Extension of Harmonic Number to Non-Integer Argument

== Theorem ==
Let $\map H x$ be the real function defined as:
:$\map H x = \gamma + \dfrac {\map {\Gamma'} {x + 1} } {\map \Gamma {x + 1} }$
where:
:$\map \Gamma x$ denotes the Gamma function
:$\map {\Gamma'} x$ denotes the derivative of the Gamma function
:$\gamma$ denotes the Euler-Mascheroni constant.
Then $H$ is an extension of the mapping $H: \N \to \Q$ defined as:
:$\forall n \in \N: \map H n = H_n$
where $H_n$ denotes the $n$th harmonic number.
== Proof ==
For $n \in \N$:
== Also see ==
* Reciprocal times Derivative of Gamma Function
== Sources ==
* : $\S 1.2.7$: Harmonic Numbers: Exercise $23$
Category:Gamma Function
Category:Harmonic Numbers
Extension of Infima Preserving Mapping to Complete Lattice Preserves Infima

== Theorem ==
Let $L_1 = \struct {S_1, \preceq_1}$, $L_2 = \struct {S_2, \preceq_2}$ be ordered sets.
Let $L_3 = \struct {S_3, \preceq_3}$ be a complete lattice.
Suppose that.
:$L_2$ is an infima inheriting ordered subset of $L_3$.
Let $f: S_1 \to S_2$ be a mapping such that:
:$f$ preserves infima.
Then
$f: S_1 \to S_3$ preserves infima.
== Proof ==
By definition of ordered subset:
:$S_2 \subseteq S_3$
Then define $g = f:S_1 \to S_3$
Let $X$ be a subset of $S_1$ such that
:$X$ admits a infimum in $L_1$.
Thus by definition of complete lattice:
:$g \sqbrk X$ admits a infimum in $L_3$.
By definition of mapping preserves infima:
:$f \sqbrk X$ admits a infimum in $L_2$ and $\map {\inf_{L_2} } {f \sqbrk X} = \map f {\map {\inf_{L_1} } X}$
Thus by definition of infima inheriting:
:$\map {\inf_{L_3} } {g \sqbrk X} = \map g {\inf_{L_1} } X$
== Sources ==
* 
Category:Order Theory
Category:Complete Lattices
Extension of Mapping/Examples/Extension of Square Function on Natural Numbers

== Example of Extension of Mapping ==
Let $f: \N \to \N$ be the mapping defined as:
:$\forall n \in \N: \map f n = n^2$
Let $h: \R \to \R$ be the mapping defined as:
:$\forall x \in \R: \map h x = x^2$
Then $h$ is a extension of $f$.
== Sources ==
* : $\S 2$: Sets and functions: Graphs and functions
Category:Examples of Extensions of Mappings
Extensive Definition/Examples/Regular Convex Polyhedra

== Examples of Extensive Definitions ==
An extensive definition for the set of regular convex polyhedra is:
:$\set {\text {tetrahedron}, \text {cube}, \text {octahedron}, \text {dodecahedron}, \text {icosahedron} }$
== Sources ==
* 
Category:Examples of Extensive Definitions
Exterior Angle of Regular Polygon

== Theorem ==
Let $P$ be a regular polygon with $n$ sides.
Then each of the exterior angles of $P$ is equal to $\dfrac {360 \degrees} n$.
== Proof ==
From Sum of External Angles of Polygon equals Four Right Angles, the sum of all $n$ exterior angles of $P$ equals $360 \degrees$.
We have that the interior angles of $P$ are equal.
Hence the exterior angles of $P$ are also equal.
Hence each exterior angle of $P$ equals $\dfrac {360 \degrees} n$.
== Sources ==
* 
* 
Category:External Angles
Exterior of Exterior of Union of Adjacent Open Intervals

== Theorem ==
Let $A$ be the union of the two adjacent open intervals:
:$A := \openint a b \cup \openint b c$
Then:
:$A^{ee} = \openint a c$
where $A^e$ is the exterior of $A$.
== Proof ==
By definition of exterior, $A^e$ is the complement relative to $\R$ of the closure of $A$ in $\R$.
Thus:
== Sources ==
* : Part $\text {II}$: Counterexamples: $32$. Special Subsets of the Real Line: $5 \ \text{(b)}$
Category:Set Exteriors
Category:Union of Adjacent Open Intervals
Exterior of Finite Union equals Intersection of Exteriors

== Theorem ==
Let $T$ be a topological space.
Let $n \in \N$.
Let $\forall i \in \closedint 1 n: H_i \subseteq T$.
Then:
:$\ds \paren {\bigcup_{i \mathop = 1}^n H_i}^e = \bigcap_{i \mathop = 1}^n H_i^e$
where $H_i^e$ denotes the exterior of $H_i$.
== Proof ==
In the following, $H_i^\circ$ denotes the interior of the set $H_i$.
== Sources ==
* : Part $\text I$: Basic Definitions: Section $1$: General Introduction: Closures and Interiors
Category:Set Exteriors
Exterior of Intersection contains Union of Exteriors

== Theorem ==
Let $T$ be a topological space.
Let $\mathbb H$ be a set of subsets of $T$.
That is, let $\mathbb H \subseteq \powerset T$ where $\powerset T$ is the power set of $T$.
Then:
:$\ds \bigcup_{H \mathop \in \mathbb H} H^e \subseteq \paren {\bigcap_{H \mathop \in \mathbb H} H}^e$
where $H^e$ denotes the exterior of $H$.
== Proof ==
We have:
From Closure of Intersection is Subset of Intersection of Closures:
:$\ds \paren {\bigcap_{H \mathop \in \mathbb H} H^-} \subseteq \bigcap_{H \mathop \in \mathbb H} H^-$
From Set Complement inverts Subsets:
:$\ds T \setminus \paren {\bigcap_{H \mathop \in \mathbb H} H^-} \supseteq T \setminus \bigcap_{H \mathop \in \mathbb H} H^-$
From the definition of exterior:
:$\ds T \setminus \paren {\bigcup_{H \mathop \in \mathbb H} H}^- = \paren {\bigcup_{H \mathop \in \mathbb H} H}^e$
Putting this together:
:$\ds \bigcup_{H \mathop \in \mathbb H} H^e \subseteq \paren {\bigcap_{H \mathop \in \mathbb H} H}^e$
== Mistakes in Sources ==
=== Union of Exteriors contains Exterior of Intersection ===
See : Part $\text I$: Basic Definitions: Section $1$: General Introduction: Closures and Interiors, where it is stated that:
== Sources ==
* : Part $\text I$: Basic Definitions: Section $1$: General Introduction: Closures and Interiors
Category:Set Exteriors
Exterior of Union of Singleton Rationals is Empty

== Theorem ==
Let $B_\alpha$ be the singleton containing the rational number $\alpha$.
Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology $\tau_d$.
Then the exterior in $\struct {\R, \tau_d}$ of the union of all $B_\alpha$ is the empty set:
:$\ds \paren {\bigcup_{\alpha \mathop \in \Q} B_\alpha}^e = \O$
== Proof ==
By definition:
:$B_\alpha = \set \alpha$
Thus:
:$\ds \bigcup_{\alpha \mathop \in \Q} B_\alpha = \Q$
By definition, the exterior of $\Q$ is the complement of the closure of $\Q$ in $\R$.
By Closure of Rational Numbers is Real Numbers:
:$\Q^- = \R$
By Relative Complement with Self is Empty Set:
:$\relcomp \R \R = \O$
Hence the result.
== Sources ==
* : Part $\text {II}$: Counterexamples: $30$. The Rational Numbers: $1$
Category:Rational Number Space
Category:Singletons
External Angle of Triangle equals Sum of other Internal Angles

== Theorem ==
The external angle of a triangle equals the sum of the other two internal angles.
== Proof 1 ==
== Proof 2 ==
== Also known as ==
== Historical Note ==
== Sources ==
* : Chapter $1$: Triangles and Polygons: Theorems and Corollaries $1.8$
* : Chapter $\text {A}.1$: Thales (ca. B.C.)
* : $(3)$
* : $(3)$
Category:External Angle of Triangle equals Sum of other Internal Angles
Category:Triangles
Category:Euclid Book I
Category:External Angles
External Angle of Triangle equals Sum of other Internal Angles/Also known as

== External Angle of Triangle equals Sum of other Internal Angles: Also known as == 
External Angle of Triangle equals Sum of other Internal Angles is referred to by some sources as the exterior angle theorem.
This, however, is also used by some sources to refer to other theorems.
In the wake of such possible confusion, it is prudent not to refer to it by name at all, but by description, as has been done on .
== Sources ==
* : Chapter $\text {A}.1$: Thales (ca. B.C.)
Category:External Angle of Triangle equals Sum of other Internal Angles
External Angle of Triangle equals Sum of other Internal Angles/Historical Note

== Historical Note ==
This theorem is the first part of Proposition $32$ of Book $\text{I}$ of .
's proposition $32$ consists of two parts: the first of which is this, and the second part of which is Sum of Angles of Triangle equals Two Right Angles.
It is not known for certain, but this theorem is traditionally ascribed to .
However, it is plausible that himself received it (either directly or indirectly) from , who may well have used it in his proof of what is now known as Thales' Theorem.
== Sources ==
* : Chapter $\text {A}.1$: Thales (ca. B.C.)
* : Chapter $\text {A}.2$: Pythagoras (ca. B.C.)
Category:Euclid Book I
Category:Historical Notes
External Angle of Triangle equals Sum of other Internal Angles/Proof 1

== Theorem ==
== Proof ==
:
Let $\triangle ABC$ be a triangle.
Let $BC$ be extended to a point $D$.
Construct $CE$ through the point $C$ parallel to the straight line $AB$.
We have that $AB \parallel CE$ and $AC$ is a transversal that cuts them.
From Parallelism implies Equal Alternate Angles:
:$\angle BAC = \angle ACE$
Similarly, we have that $AB \parallel CE$ and $BD$ is a transversal that cuts them.
From Parallelism implies Equal Corresponding Angles:
:$\angle ECD = \angle ABC$
Thus by Euclid's Second Common Notion:
: $\angle ACD = \angle ABC + \angle BAC$
== Historical Note ==
== Sources ==
* : Book $\text{I}$. Propositions
Category:External Angle of Triangle equals Sum of other Internal Angles
External Angle of Triangle equals Sum of other Internal Angles/Proof 2

== Theorem ==
== Proof ==
Let $\triangle ABC$ be a triangle.
From Sum of Angles of Triangle equals Two Right Angles: Proof 2:
:$\paren 1: \angle ABC + \angle BCA + \angle CAB = 180^\circ$
Extend $AB$ to $D$.
By Two Angles on Straight Line make Two Right Angles:
:$\paren 1: \angle ABC + \angle CBD = 180^\circ$
Combining $\paren 1$ and $\paren 2$ and using Equality is Transitive:
:$\angle ABC + \angle BCA + \angle CAB = \angle ABC + \angle CBD$
By using commom notion 3:
:$\angle BCA + \angle CAB = \angle CBD$
By using Equality is Symmetric:
:$\angle CBD = \angle BCA + \angle CAB$
Category:External Angle of Triangle equals Sum of other Internal Angles
External Angle of Triangle is Greater than Internal Opposite

== Theorem ==
The external angle of a triangle is greater than either of the opposite internal angles.
== Proof ==
:
Let $\triangle ABC$ be a triangle.
Let the side $BC$ be extended to $D$.
Let $AC$ be bisected at $E$.
Let $BE$ be joined and extended to $F$.
Let $EF$ be made equal to $BE$.
(Technically we really need to extend $BE$ to a point beyond $F$ and then crimp off a length $EF$.)
Let $CF$ be joined.
Let $AC$ be extended to $G$.
We have $\angle AEB = \angle CEF$ from Two Straight Lines make Equal Opposite Angles.
Since $AE = EC$ and $BE = EF$, from Triangle Side-Angle-Side Congruence we have $\triangle ABE = \triangle CFE$.
Thus $AB = CF$ and $\angle BAE = \angle ECF$.
But $\angle ECD$ is greater than $\angle ECF$.
Therefore $\angle ACD$ is greater than $\angle BAE$.
Similarly, if $BC$ were bisected, $\angle BCG$, which is equal to $\angle ACD$ by Two Straight Lines make Equal Opposite Angles, would be shown to be greater than $\angle ABC$ as well.
Hence the result.
== Sources ==
* : Book $\text{I}$. Propositions
* : Chapter $1$: Triangles and Polygons: Theorems and Corollaries $1.8$: Corollary $2$
Category:Triangles
Category:External Angles