avewright/proofwiki-math huggingface dataset:
Theorem: Ring of Integers of Algebraic Number Field is UFD iff Class Number is 1

Let $K$ be a field of algebraic numbers.
Let $\OO_K$ be the ring of integers of $K$.
Then $\OO_K$ is a unique factorization domain (UFD) {{iff}} the class number of $K$ is $1$.

Proof:
{{ProofWanted|This may already exist in some form in {{ProofWiki}}. This will need to be ascertained by someone fluent in the language of algebraic number fields.}}
Theorem: Area of Triangle Inscribed in Parabola

Let $T$ be the parabola which is
the locus of points $\tuple {x, y}$ satisfying $y = x^2$.
Let $A$ and $B$ be two arbitrary points on $T$ with coordinates:
:$A = \tuple {u, u^2}$
:$B = \tuple {v, v^2}$, with $u > v$
Let $C$ be a third point on $T$ whose $x$-coordinate is the average of those of $A$ and $B$.
The area of $\triangle ABC$ is:
:$\map \AA {\triangle ABC} = \dfrac 1 8 \paren {u - v}^3$

Proof:
The point $\tuple {x = 0, y = 0}$ satisfies $y = x^2$.
Since $x^2 \ge 0$, $0$ is the minimum value for $y$.
Thus, the vertex of $T$ lies at the origin.
The coordinates of $C$ are given as the average those for $A$ and $B$.
Given:
:$A = \tuple {u, u^2}$
:$B = \tuple {v, v^2}$, with $u > v$
By the definition of average: 
:$C = \tuple {\dfrac 1 2 \paren {u + v}, \dfrac 1 4 \paren {u + v}^2 } $
Let $P$ be the midpoint of $AB$, such that $AP = BP$.
Let the coordinates of $P$ be $\tuple {P_x, P_y}$.
By the Midline Theorem:
:$P_x = \dfrac 1 2 \paren {u + v}$
Also by the Midline Theorem:
:$P_y = \dfrac 1 2 \paren {u^2 + v^2}$
Let $h$ be one-half the distance between the $x$-coordinates of $A$ and $B$:
:$h = \dfrac 1 2 \paren {u - v}$
By construction:
:the height of both $\triangle APC$ and $\triangle BPC$ is equal to $h$.
Let $b$ be the length of $PC$, the shared base of $\triangle APC$ and $\triangle BPC$.
{{begin-eqn}} 
{{eqn | l = b
      | r = P_y - C_y
      | c = Definition above
}}
{{eqn | l = b
      | r = \dfrac 1 2 \paren {u^2 + v^2} - \dfrac 1 4 \paren {u + v}^2
      | c = Substitution
}}
{{eqn | l = b
      | r = \dfrac 1 4 \paren {2 u^2 + 2 v^2 - \paren {u + v}^2}
      | c = Factor out $\dfrac 1 2$
}}
{{eqn | l = b
      | r = \dfrac 1 4 \paren {u^2 - 2 u v + v^2}
      | c = Expansion and subtraction
}}
{{eqn | l = b
      | r = \dfrac 1 4 \paren {u - v}^2
      | c = Factor
}}
{{end-eqn}}
{{:Euclid:Proposition/I/38}}
By Area of Triangle:
:$\map \AA {\triangle APC} = \dfrac 1 2 h b$
Substituting from above:
:$\map \AA {\triangle APC} = \dfrac 1 {16} \paren {u - v}^3$
Since they have the same height and a shared base:
:$\map \AA {\triangle APC} = \map \AA {\triangle BPC}$
But:
:$\map \AA {\triangle ABC} = \map \AA {\triangle APC} + \map \AA {\triangle BPC}$
By addition:
:$\map \AA {\triangle ABC} = h b = \dfrac 1 8 \paren {u - v}^3$
{{qed}}
Theorem: Ring of Bounded Continuous Functions is Subring 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}, +, *}$ 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}, +, *}$ is a subring of $\struct {\map C {S, \R}, +, *}$

Proof:
From Ring of Continuous Real-Valued Functions is Ring:
:$\struct {\map C {S, \R}, +, *}$ is a ring.
From Additive Inverse in Ring of Continuous Real-Valued Functions:
:$\forall f \in R^S :$ the additive inverse of $f$ is the pointwise negation $-f$, defined by:
::$\forall s \in S: \map {\paren {-f} } s := - \map f s$
From the Subring Test:
:$\struct {\map {C^*} {S, \R}, +, *}$ is a subring of $\struct {\map C {S, \R}, +, *}$
{{iff}}
:$(1) \quad \map {C^*} {S, R} \ne \O$
:$(2) \quad \forall f, g \in \map {C^*} {S, R} : f + \paren{-g} \in  \map {C^*} {S, R}$
:$(3) \quad \forall f, g \in \map {C^*} {S, R} : f * g \in  \map {C^*} {S, R}$
Theorem: Zero of Ring of Bounded 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}, +, *}$ be the ring of bounded continuous real-valued functions from $S$.
Then:
:the zero of $\struct{\map {C^*} {S, \R}, +, *}$ is the constant mapping $0_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {0_{\R^S}} s = 0$

Proof:
Let $\struct{\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
From Ring of Bounded Continuous Functions is Subring of Continuous Real-Valued Functions:
:$\struct{\map {C^*} {S, \R}, +, *}$ is a subring of $\struct{\map C {S, \R}, +, *}$
From Zero of Ring of Continuous Real-Valued Functions:
:the zero of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $0_{\R^S} : S \to R$ defined by:
::$\forall s \in S : \map {0_{\R^S}} s = 0$
From Zero of Subring is Zero of Ring:
:$0_{\R^S}$ is the zero of $\struct{\map {C^*} {S, \R}, +, *}$
{{qed}}
Theorem: Unity of Ring of Bounded 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}, +, *}$ be the ring of bounded continuous real-valued functions from $S$.
Then:
:the unity of $\struct{\map {C^*} {S, \R}, +, *}$ is the constant mapping $1_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {1_{\R^S}} s = 1$.

Proof:
Let $\struct{\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
From Ring of Bounded Continuous Functions is Subring of Continuous Real-Valued Functions:
:$\struct{\map {C^*} {S, \R}, +, *}$ is a subring of $\struct{\map C {S, \R}, +, *}$
From Unity of Ring of Continuous Real-Valued Functions:
:the unity of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $1_{\R^S} : S \to R$ defined by:
::$\forall s \in S : \map {1_{\R^S}} s = 1$
From Constant Mapping is Continuous and Constant Real-Valued Function is Bounded:
:$1_{\R^S} \in \map {C^*} {S, \R}$
From Subring Containing Ring Unity has Unity:
:$1_{\R^S}$ is the unity of $\struct{\map {C^*} {S, \R}, +, *}$
{{qed}}
Theorem: Ring of Bounded Continuous Real-Valued Functions is Commutative

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

Proof:
Let $\struct{\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
From Ring of Bounded Continuous Functions is Subring of Continuous Real-Valued Functions:
:$\struct{\map {C^*} {S, \R}, +, *}$ is a subring of $\struct{\map C {S, \R}, +, *}$
From Ring of Continuous Real-Valued Functions is Commutative:
:$\struct{\map C {S, \R}, +, *}$ is a commutative ring
From Subring of Commutative Ring is Commutative:
:$\struct{\map {C^*} {S, \R}, +, *}$ is a commutative ring
{{qed}}
Theorem: Zero of Ring 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}, +, *}$ be the ring of continuous real-valued functions from $S$.
Then:
:the zero of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $0_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {0_{\R^S}} s = 0$

Proof:
By definition of ring of continuous real-valued functions:
:$\struct {\map C {S, \R}, +, *}$ is the ring of continuous mappings from $S$ to $\R$.
From Zero of Ring of Continuous Mappings:
:the zero of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $0_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {0_{\R^S}} s = 0$
{{qed}}
Theorem: Unity of Ring 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}, +, *}$ be the ring of continuous real-valued functions from $S$.
Then:
:the unity of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $1_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {1_{\R^S}} s = 1$.

Proof:
By definition of ring of continuous real-valued functions:
:$\struct {\map C {S, \R}, +, *}$ is the ring of continuous mappings from $S$ to $\R$.
From Unity of Ring of Continuous Mappings:
:the unity of $\struct{\map C {S, \R}, +, *}$ is the constant mapping $1_{\R^S} : S \to \R$ defined by:
::$\forall s \in S : \map {1_{\R^S}} s = 1$.
{{qed}}
Theorem: Ring of Continuous Real-Valued Functions is Commutative

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

Proof:
By definition of ring of continuous real-valued functions:
:$\struct {\map C {S, \R}, +, *}$ is the ring of continuous mappings from $S$ to $\R$.
From Commutativity of Ring of Continuous Mappings:
:$\struct{\map C {S, \R}, +, *}$ is a commutative ring
{{qed}}
Theorem: Ring of Continuous Real-Valued Functions is Ring

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

Proof:
By definition of ring of continuous real-valued functions:
:$\struct {\map C {S, \R}, +, *}$ is the ring of continuous mappings from $S$ to $\R$.
From Ring of Continuous Mappings is Subring of All Mappings:
:$\struct {\map C {S, \R}, +, *}$ is a subring
By definition of subring:
:$\struct {\map C {S, \R}, +, *}$ is a ring
{{qed}}
Theorem: Cone on Compact Space is Compact

Let $A$ be a compact topological space.
Let $C A$ denote the cone on $A$.
Then, $C A$ is compact.

Proof:
By definition of cone:
:$C A = T \ast A$
where:
:$T$ denotes the trivial topological space
:$T \ast A$ denotes the join of $T$ and $A$
By Finite Topological Space is Compact, $T$ is compact.
Therefore, by Join of Compact Spaces is Compact:
:$C A$ is compact.
{{qed}}
Category:Compact Topological Spaces
jmdxk0frvkvoqotn5vg3d3urb0kwx4l
Theorem: Euler Phi Function of Product

Let $m$ and $n$ be positive integers.
Let $d$ be the greatest common divisor of $m$ and $n$.
Then:
:$\map \phi {m n} = \map \phi m \map \phi n \paren {\dfrac d {\map \phi d} }$
where $\phi$ is the Euler $\phi$ function.

Proof:
From Euler Phi Function of Integer, we have:
:$\ds \frac {\map \phi m} m = \prod_{p \mathop \divides m} \paren {1 - \frac 1 p}$
:$\ds \frac {\map \phi n} n = \prod_{p \mathop \divides n} \paren {1 - \frac 1 p}$
:$\ds \frac {\map \phi {m n} } {m n} = \prod_{p \mathop \divides m n} \paren {1 - \frac 1 p}$
where the products are understood to run over the primes.
We consider:
:$\ds \paren {\prod_{p \mathop \divides m} \paren {1 - \frac 1 p} } \paren {\prod_{p \mathop \divides n} \paren {1 - \frac 1 p} }$
and its relation to:
:$\ds \prod_{p \mathop \divides m n} \paren {1 - \frac 1 p}$
From Euclid's Lemma for Prime Divisors, a prime $p$ divides $m n$ {{iff}} $p$ divides at least one of $m$ or $n$.
So every term in the product:
:$\ds \prod_{p \mathop \divides m n} \paren {1 - \frac 1 p}$
is included within:
:$\ds \paren {\prod_{p \mathop \divides m} \paren {1 - \frac 1 p} } \paren {\prod_{p \mathop \divides n} \paren {1 - \frac 1 p} } = \Pi$
If $p$ divides exactly one of $m$ or $n$, $\paren {1 - \dfrac 1 p}$ will appear exactly once in the product $\Pi$.
If $p$ divides both of $m$ and $n$, then $\paren {1 - \dfrac 1 p}$ will appear twice in the product $\Pi$.
From the definition of the greatest common divisor, $p$ divides both of $m$ and $n$ {{iff}} it divides $d$.
Hence, removing the extraneous terms from $\Pi$ we obtain:
:$\ds \prod_{p \mathop \divides m n} \paren {1 - \frac 1 p} = \frac { \paren {\prod_{p \mathop \divides m} \paren {1 - \frac 1 p} } \paren {\prod_{p \mathop \divides n} \paren {1 - \frac 1 p} } } {\prod_{p \mathop \divides d} \paren {1 - \frac 1 p} }$
From Euler Phi Function of Integer, we have:
:$\ds \prod_{p \mathop \divides d} \paren {1 - \frac 1 p} = \frac {\map \phi d} d$
So, we obtain:
:$\dfrac {\map \phi {m n} } {m n} = \dfrac {\frac {\map \phi m \map \phi n} {m n} } {\frac {\map \phi d} d} = \dfrac 1 {m n} \paren {\map \phi m \map \phi n \paren {\dfrac d {\map \phi d} } }$
Hence:
:$\map \phi {m n} = \map \phi m \map \phi n \paren {\dfrac d {\map \phi d} }$
as required.
{{qed}}
Category:Euler Phi Function
twejwqeylkx8y732ogj2b7arb5xbpkq
Theorem: Parallel Chords Cut Equal Chords in a Circle

Let $\CC$ be a circle on center $O$.
Let $AB$ and $CD$ be chords in $\CC$ with $AB \parallel CD$.
Then the two chords  cut from the circle by $AB$ and $CD$ are equal:
:$AC = BD$

Proof:
300px
Draw $AD$.
By Parallelism implies Equal Alternate Angles:
:$\angle BAD = \angle ADC$
The central angles corresponding to $\angle BAD$ and $\angle ADC$ are equal by Inscribed Angle Theorem:
:$\angle BOD = \angle AOC$
As radii of $\CC$:
:$OB = OD = OC = OA$
By Triangle Side-Angle-Side Congruence:
:$\triangle OAC \cong \triangle OBD$
So:
:$AC = BD$
{{qed}}
Category:Circles
Category:Parallel Lines
5fcwzfh9lm4wvm4qsijasfvs6h84k99
Theorem: Cofunction of Cofunction

Let $g$ be a cofunction of $f$.
Then $f$ is a cofunction of $g$.
That is, cofunctions exist in pairs.

Proof:
That is:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \map g x
      | r = \map f {90 \degrees - x}
      | c = {{Defof|Cofunction}}
}}
{{eqn | l = \map g {90 \degrees - x}
      | r = \map f {90 \degrees - \paren {90 \degrees - x} }
      | c = 
}}
{{eqn | r = \map f x
      | c = 
}}
{{end-eqn}}
Hence the result by definition of cofunction.
{{qed}}
Theorem: Sine and Cosine are Cofunctions

The sine and cosine are cofunctions:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \sin x
      | r = \map \cos {90 \degrees - x}
}}
{{eqn | l = \cos x
      | r = \map \sin {90 \degrees - x}
}}
{{end-eqn}}

Proof:
We have:
:Sine of Complement equals Cosine
:Cosine of Complement equals Sine
Hence the result by definition of cofunction.
{{qed}}
Theorem: Tangent and Cotangent are Cofunctions

The tangent and cotangent are cofunctions:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x \in \R, \cos x \ne 0
      | l = \tan x
      | r = \map \cot {90 \degrees - x}
}}
{{eqn | n = 2
      | q = \forall x \in \R, \sin x \ne 0
      | l = \cot x
      | r = \map \tan {90 \degrees - x}
}}
{{end-eqn}}

Proof:
=== Proof of $(1)$ ===
From Tangent is Sine divided by Cosine:
:$\tan x = \dfrac {\sin x} {\cos x}$
Hence in order for $\tan x$ to be defined it is necessary for $\cos x \ne 0$.
Then we have:
:Tangent of Complement equals Cotangent
{{qed|lemma}}
Theorem: Secant and Cosecant are Cofunctions

The secant and cosecant are cofunctions:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x \in \R, \cos x \ne 0
      | l = \sec x
      | r = \map \csc {90 \degrees - x}
}}
{{eqn | n = 2
      | q = \forall x \in \R, \sin x \ne 0
      | l = \csc x
      | r = \map \sec {90 \degrees - x}
}}
{{end-eqn}}

Proof:
=== Proof of $(1)$ ===
From Secant is Reciprocal of Cosine:
:$\sec x = \dfrac 1 {\cos x}$
Hence in order for $\sec x$ to be defined it is necessary for $\cos x \ne 0$.
Then we have:
:Secant of Complement equals Cosecant
{{qed|lemma}}
Theorem: Kinetic Energy is not necessarily Conserved in a Collision

Let two bodies be in collision.
The total kinetic energy of the two bodies before the collision may not necessarily be the same as the total kinetic energy of the two bodies after the collision.

Proof:
{{ProofWanted|some background work needed here}}
Theorem: Column Rank of Matrix equals Row Rank

Let $\mathbf A$ be a matrix.
The column rank of $\mathbf A$ is equal to the row rank of $\mathbf A$.

Proof:
=== Proof Outline and Definitions ===
Recall:
:The row rank of $\mathbf A$ is defined as the dimension of the row space.
:The column rank of $\mathbf A$ is defined as the dimension of the column space.
{{WLOG}}, we define the rank of $\mathbf A$ to be the column rank of $\mathbf A$.
{{ExtractTheorem|We announce and prove results like the following by means of a separate page dedicated to that result. Please review the design philosophy of {{ProofWiki}}.}}
{{Recall|Transpose of Matrix}}
{{:Definition:Transpose of Matrix}}
That is, the columns of a matrix are the rows of its transpose and the rows of a matrix are the columns of its transpose.
Thus, Row Rank of Transpose is Column Rank and of course Column Rank of Transpose is Row Rank:
:$\map r {\mathbf A} = \map c {\mathbf A^\intercal}$
:$\map c {\mathbf A} = \map r {\mathbf A^\intercal}$
where $\map r {\mathbf A}$ and $\map c {\mathbf A}$ denote the row rank and column rank respectively.
Hence this result is equivalent to:
:$\map c {\mathbf A} = \map c {\mathbf A^\intercal}$
where $\mathbf A^\intercal$ denotes the transpose of $\mathbf A$.
Theorem: Column Rank of Matrix equals Row Rank

Let $\mathbf A$ be a matrix.
The column rank of $\mathbf A$ is equal to the row rank of $\mathbf A$.

Proof:
Let $\map c {\mathbf A}$ denote the column rank of $\mathbf A$.
Let $\map r {\mathbf A}$ denote the row rank of $\mathbf A$.
Let $\mathbf A$ be an $m\times n$ matrix whose row rank is $r$.
Therefore, the dimension of the row space of $\mathbf A$ is $r$.
Let $\mathbf x_1, \ldots, \mathbf x_r$ be a basis of the row space of $\mathbf A$.
We claim that the vectors $\mathbf A \mathbf x_1, \ldots, \mathbf A \mathbf x_r$ are linearly independent.
To see why, consider the following linear combination of these vectors with scalar coefficients $c_1, \ldots, c_r$:
:$\mathbf 0 = c_1 \mathbf A \mathbf x_1 + c_2 \mathbf A \mathbf x_2 + \cdots + c_r \mathbf A \mathbf x_r = \mathbf A \paren {c_1 \mathbf x_1 + c_2 \mathbf x_2 + \cdots + c_r \mathbf x_r} = \mathbf A \mathbf v$
where $\mathbf v = c_1 \mathbf x_1 + \cdots + c_r \mathbf x_r$.
We make two observations:
:$(\text a) \mathbf v$ is a linear combination of vectors in the row space of $\mathbf A$, which implies that $\mathbf v$ belongs to the row space of $\mathbf A$
:$(\text b)$ since $\mathbf A \mathbf v = \mathbf 0$, the vector $\mathbf v$ is orthogonal to every row vector of $\mathbf A$ and, hence, is orthogonal to every vector in the row space of $\mathbf A$.
The facts $(\text a)$ and $(\text b)$ together imply that $\mathbf v$ is orthogonal to itself, which proves that $\mathbf v = \mathbf 0$.
Therefore:
:$c_1 \mathbf x_1 + c_2 \mathbf x_2 + \cdots + c_r \mathbf x_r = \mathbf 0$
But recall that $\mathbf x_1, \ldots, \mathbf x_r$ were chosen as a basis of the row space of $\mathbf A$ and so are linearly independent.
This implies that
:$c_1 = \cdots = c_r = 0$
It follows that $\mathbf A \mathbf x_1,\ldots, \mathbf A \mathbf x_r$ are linearly independent.
Now, $\mathbf A \mathbf x_1, \ldots, \mathbf A \mathbf x_r$ are vectors in the column space of $\mathbf A$.
From the above argument, they are also $r$ linearly independent vectors in the column space of $\mathbf A$.
Therefore, the dimension of the column space of $\mathbf A$ (that is, the column rank of $\mathbf A$) must be at least as big as $r$.
This proves that $\map r {\mathbf A} \le \map c {\mathbf A}$, that is, row rank of $\mathbf A$ is no larger than the column rank of $\mathbf A$.
This result applies to any matrix $\mathbf{A}$.
So, we can apply this result to the transpose of $\mathbf A$ to get the reverse inequality:
:$\map r {\mathbf A^\intercal} \le \map c {\mathbf A^\intercal}$
Combining these inequalities, we conclude that row rank equals column rank as follows:
:$\map r {\mathbf A} \le \map c {\mathbf A} = \map r {\mathbf A^\intercal} \le \map c {\mathbf A^\intercal} = \map r {\mathbf A}$
{{qed}}
Theorem: Column Rank of Matrix equals Row Rank

Let $\mathbf A$ be a matrix.
The column rank of $\mathbf A$ is equal to the row rank of $\mathbf A$.

Proof:
Let $\map c {\mathbf A}$ denote the column rank of $\mathbf A$.
Let $\map r {\mathbf A}$ denote the row rank of $\mathbf A$.
Let $\mathbf A$ be an $m \times n$ matrix whose column rank is $r$.
Therefore, the dimension of the column space of $\mathbf A$ is $r$.
Let $\mathbf c_1, \ldots, \mathbf c_r$ be any basis for the column space of $\mathbf A$.
Place these vectors as column vectors to form the $m \times r$ matrix $\mathbf C = \begin {bmatrix} \mathbf c_1 & \mathbf c_2 & \cdots & \mathbf c_r \end{bmatrix}$.
Therefore, every column vector of $\mathbf A$ is a linear combination of the columns of $\mathbf C$.
To be precise, if $\mathbf A = \begin {bmatrix} \mathbf a_1 & \mathbf a_2 & \cdots & \mathbf a_n \end {bmatrix}$ is an $m \times n$ matrix with $\mathbf a_j$ as the $j$-th column, then: 
:$\mathbf a_j = f_{1j} \mathbf c_1 + f_{2j} \mathbf c_2 + \cdots + f_{rj} \mathbf c_r \text { for } j = 1, \ldots, n$
where $f_{ij}$ are the scalar coefficients of $\mathbf a_j$ in terms of the basis $\mathbf c_1, \mathbf c_2, \ldots, \mathbf c_r$.
This implies that:
:$\mathbf A = \mathbf C \mathbf F$
where $f_{ij}$ is the $\tuple {i, j}$th element of $\mathbf F$. 
Using transposition of products, we note that $\mathbf A^\intercal = \mathbf F^\intercal \mathbf C^\intercal$.
From the definition of matrix multiplication, this means that each column of $\mathbf A^\intercal$ is a linear combination of the columns of $\mathbf F^\intercal$.
Therefore, the column space of $\mathbf A^\intercal$ is a subspace of the column space of $\mathbf F^\intercal$.
Hence:
:$\map c {\mathbf A^\intercal} \le \map c {\mathbf F^\intercal}$
Now, $\mathbf F^\intercal$ is $n \times r$
Thus there are $r$ columns in $\mathbf F^\intercal$.
Hence:
:$\map c {\mathbf A^\intercal} \le r = \map c {\mathbf A}$
This proves that $\map c {\mathbf A^\intercal} \le \map c {\mathbf A}$.
Now apply the result to the matrix $\mathbf A^\intercal$ to obtain the reverse inequality:
Since $\paren {\mathbf A^\intercal}^\intercal = \mathbf A$, we can write:
:$\map c {\mathbf A} = \map c {\paren {\mathbf A^\intercal}^\intercal} \le \map c {\mathbf A^\intercal}$
This proves $\map c {\mathbf A} \le \map c {\mathbf A^\intercal}$.
We have, therefore, proved:
:$\map c {\mathbf A^\intercal} \le \map c {\mathbf A}$
and the reverse inequality:
:$\map c {\mathbf A} \le \map c {\mathbf A^\intercal}$
Therefore:
:$\map c {\mathbf A} = \map c {\mathbf A^\intercal}$
{{qed}}
Theorem: Column Rank of Matrix equals Rank of Matrix

Let $\mathbf A$ be a matrix.
The column rank of $\mathbf A$ is equal to the rank of $\mathbf A$.

Proof:
The rank of $\mathbf A$ is defined as the dimension of the column space of $\mathbf A$.
Thus the result follows by definition.
{{qed}}
Theorem: Constant Real-Valued Function is Bounded

Let $S$ be a set.
Let $\R$ denote the real number line.
Let $c \in \R$.
Let $c_{\R^S} : S \to R$ be the constant mapping defined by:
:$\forall s \in S : \map {c_{\R^S} } s = c$
Then $c_{\R^S}$ is a bounded real-valued function.

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \size{\map {c_{\R^S} } s} 
      | r = \size c
      | c = {{Defof|Constant Mapping}}
}}
{{eqn | o = \le 
      | r = \size c
}}
{{end-eqn}}
It follows that $c_{\R^S}$ is a bounded real-valued function by definition.
{{qed}}
Category:Constant Mappings
Category:Bounded Real-Valued Functions
lwn4d2yp6japlvwvzkb4ss7h2izzgs6
Theorem: Refinement of Open Cover has Greater Entropy

Let $X$ be a compact topological space.
Let $\alpha, \beta$ be open covers of $X$.
Let $\map H \alpha$ and $\map H \beta$ be their entropies.
Suppose that $\beta$ is a refinement of $\alpha$.
Then:
:$\map H \alpha \le \map H \beta$

Proof:
By definition of entropy of open cover, there is a finite subcover $\beta' \subseteq \beta$ such that:
:$\map H \beta = \map \ln k$
with $k = \size {\beta '}$.
We write:
:$\beta' = \set {B_1, \ldots, B_k}$
{{Recall|Refinement of Cover}}
:$\forall i \in \set {1, \ldots ,k} \; \exists A_i \in \alpha : B_i \subseteq A_i$
Then:
:$\alpha' = \set {A_1, \ldots, A_k}$
is a subcover of $\alpha$.
Thus, by definition of entropy of open cover:
:$\map H \alpha \le \map \ln k = \map H \beta$
{{qed}}