avewright/proofwiki-math huggingface dataset:
Theorem: Determinant of Elementary Column Matrix/Scale Column

Let $e_1$ be the elementary column operation $\text {ECO} 1$:
{{begin-axiom}}
{{axiom | n = \text {ECO} 1
        | t = For some $\lambda \ne 0$, multiply column $k$ by $\lambda$
        | m = \kappa_k \to \lambda \kappa_k
}}
{{end-axiom}}
which is to operate on some arbitrary matrix space.
Let $\mathbf E_1$ be the elementary column matrix corresponding to $e_1$.
The determinant of $\mathbf E_1$ is:
:$\map \det {\mathbf E_1} = \lambda$

Proof:
By Elementary Matrix corresponding to Elementary Column Operation: Scale Column, the elementary column matrix corresponding to $e_1$ is of the form:
:$E_{a b} = \begin {cases} \delta_{a b} & : a \ne k \\ \lambda \cdot \delta_{a b} & : a = k \end{cases}$
where:
:$E_{a b}$ denotes the element of $\mathbf E_1$ whose indices are $\tuple {a, b}$
:$\delta_{a b}$ is the Kronecker delta:
::$\delta_{a b} = \begin {cases} 1 & : \text {if $a = b$} \\ 0 & : \text {if $a \ne b$} \end {cases}$
Thus when $a \ne b$, $E_{a b} = 0$.
This means that $\mathbf E_1$ is a diagonal matrix.
{{begin-eqn}}
{{eqn | l = \ds \map \det {\mathbf E_1}
      | r = \prod_i E_{i i}
      | c = Determinant of Diagonal Matrix
      | cc= where the index variable $i$ ranges over the order of $\mathbf E_1$
}}
{{eqn | r = \prod_i \paren {\begin {cases} 1 & : i \ne k \\ \lambda & : a = k \end{cases} }
      | c = 
}}
{{eqn | r = \prod_{i \mathop \ne k} 1 \times \prod_{i \mathop = k} \lambda
      | c = 
}}
{{eqn | r = 1 \times \lambda
      | c = 
}}
{{eqn | r = \lambda
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Determinant of Elementary Column Matrix/Scale Column and Add

Let $e_2$ be the elementary column operation $\text {ECO} 2$:
{{begin-axiom}}
{{axiom | n = \text {ECO} 2
        | t = For some $\lambda$, add $\lambda$ times column $j$ to column $i$
        | m = \kappa_i \to \kappa_i + \lambda \kappa_j
}}
{{end-axiom}}
which is to operate on some arbitrary matrix space.
Let $\mathbf E_2$ be the elementary column matrix corresponding to $e_2$.
The determinant of $\mathbf E_2$ is:
:$\map \det {\mathbf E_2} = 1$

Proof:
By Elementary Matrix corresponding to Elementary Column Operation: Scale Column and Add, $\mathbf E_2$ is of the form:
:$E_{a b} = \delta_{a b} + \lambda \cdot \delta_{b i} \cdot \delta_{j a}$
where:
:$E_{a b}$ denotes the element of $\mathbf E$ whose indices are $\tuple {a, b}$
:$\delta_{a b}$ is the Kronecker delta:
::$\delta_{a b} = \begin {cases} 1 & : \text {if $a = b$} \\ 0 & : \text {if $a \ne b$} \end {cases}$
Because $i \ne j$ it follows that:
:if $a = i$ and $b = j$ then $a \ne b$
Hence when $a = b$ we have that:
:$\delta_{b i} \cdot \delta_{j a} = 0$
Hence the diagonal elements of $\mathbf E_2$ are all equal to $1$.
We also have that $\delta_{b i} \cdot \delta_{j a} = 1$ {{iff}} $a = i$ and $b = j$.
Hence, all elements of $\mathbf E_2$ apart from the diagonal elements and $a_{i j}$ are equal to $0$.
Thus $\mathbf E_2$ is a triangular matrix (either upper or lower).
From Determinant of Triangular Matrix, $\map \det {\mathbf E_2}$ is equal to the product of all the diagonal elements of $\mathbf E_2$.
But as we have seen, these are all equal to $1$.
Hence the result.
{{qed}}
Theorem: Multiple of Column Added to Column of Determinant

Let <nowiki>$\mathbf A = \begin {bmatrix}
a_{1 1} & \cdots & a_{1 r} & \cdots & a_{1 s} & \cdots & a_{1 n} \\
a_{2 1} & \cdots & a_{2 r} & \cdots & a_{2 s} & \cdots & a_{2 n} \\
 \vdots & \ddots &  \vdots & \ddots &  \vdots & \ddots &  \vdots \\
a_{n 1} & \cdots & a_{n r} & \cdots & a_{n s} & \cdots & a_{n n} \\
\end {bmatrix}$</nowiki> be a square matrix of order $n$.
Let $\map \det {\mathbf A}$ denote the determinant of $\mathbf A$.
Let <nowiki>$\mathbf B = \begin{bmatrix}
a_{1 1} & \cdots & a_{1 r} + \lambda a_{1 s} & \cdots & a_{1 s} & \cdots & a_{1 n} \\
a_{2 1} & \cdots & a_{2 r} + \lambda a_{2 s} & \cdots & a_{2 s} & \cdots & a_{2 n} \\
 \vdots & \ddots &                    \vdots & \ddots &  \vdots & \ddots &  \vdots \\
a_{n 1} & \cdots & a_{n r} + \lambda a_{n s} & \cdots & a_{n s} & \cdots & a_{n n} \\
\end{bmatrix}$</nowiki>.
Then $\map \det {\mathbf B} = \map \det {\mathbf A}$.
That is, the value of a determinant remains unchanged if a constant multiple of any column is added to any other column.

Proof:
We have that:
:<nowiki>$\mathbf A^\intercal = \begin {bmatrix}
a_{1 1} & a_{1 2} & \cdots & a_{1 n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{r 1} & a_{r 2} & \cdots & a_{r n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{s 1} & a_{s 2} & \cdots & a_{s n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n n} \\
\end {bmatrix}$</nowiki>
where $\mathbf A^\intercal$ denotes the transpose of $\mathbf A$.
Similarly, we have that:
:<nowiki>$\mathbf B^\intercal = \begin{bmatrix}
a_{1 1} & a_{1 2} & \ldots & a_{1 n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{r 1} + \lambda a_{s 1} & a_{r 2} + \lambda a_{s 2} & \cdots & a_{r n} + \lambda a_{s n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{s 1} & a_{s 2} & \cdots & a_{s n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n n} \\
\end {bmatrix}$</nowiki>
From Multiple of Row Added to Row of Determinant:
:$\map \det {\mathbf B^\intercal} = \map \det {\mathbf A^\intercal}$
From from Determinant of Transpose:
:$\map \det {\mathbf B^\intercal} = \map \det {\mathbf B}$
:$\map \det {\mathbf A^\intercal} = \map \det {\mathbf A}$
and the result follows.
{{qed}}
Theorem: Determinant with Column Multiplied by Constant

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
Let $\map \det {\mathbf A}$ be the determinant of $\mathbf A$.
Let $\mathbf B$ be the matrix resulting from one column of $\mathbf A$ having been multiplied by a constant $c$.
Then:
:$\map \det {\mathbf B} = c \map \det {\mathbf A}$
That is, multiplying one column of a square matrix by a constant multiplies its determinant by that constant.

Proof:
Let:
:<nowiki>$\mathbf A = \begin{bmatrix}
a_{1 1} & a_{1 2} & \cdots & a_{1 r} & \cdots & a_{1 n} \\
a_{2 1} & a_{2 2} & \cdots & a_{2 r} & \cdots & a_{2 n} \\
 \vdots &  \vdots & \ddots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n r} & \cdots & a_{n n} \\
\end{bmatrix}$</nowiki>
:<nowiki>$\mathbf B = \begin{bmatrix}
b_{1 1} & b_{1 2} & \cdots & b_{1 r} & \cdots & b_{1 n} \\
b_{2 1} & b_{2 2} & \cdots & b_{2 r} & \cdots & b_{1 n} \\
 \vdots &  \vdots & \ddots &  \vdots & \ddots &  \vdots \\
b_{n 1} & b_{n 2} & \cdots & b_{n r} & \cdots & b_{n n} \\
\end{bmatrix} = \begin{bmatrix}
a_{1 1} & a_{1 2} & \cdots & c a_{1 r} & \cdots & a_{1 n} \\
a_{2 1} & a_{2 2} & \cdots & c a_{2 r} & \cdots & a_{1 n} \\
 \vdots &  \vdots & \ddots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n r} & \cdots & a_{n n} \\
\end{bmatrix}$</nowiki>
We have that:
:<nowiki>$\mathbf A^\intercal = \begin {bmatrix}
a_{1 1} & a_{1 2} & \cdots & a_{1 n} \\
a_{2 1} & a_{2 2} & \cdots & a_{2 n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{r 1} & a_{r 2} & \cdots & a_{r n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n n} \\
\end {bmatrix}$</nowiki>
where $\mathbf A^\intercal$ denotes the transpose of $\mathbf A$.
Similarly, we have that:
:<nowiki>$\mathbf B^\intercal = \begin{bmatrix}
a_{1 1} & a_{1 2} & \ldots & a_{1 n} \\
a_{2 1} & a_{2 2} & \ldots & a_{2 n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
c a_{r 1} & c a_{r 2} & \cdots & c a_{r n} \\
 \vdots &  \vdots & \ddots &  \vdots \\
a_{n 1} & a_{n 2} & \cdots & a_{n n} \\
\end {bmatrix}$</nowiki>
From Determinant with Row Multiplied by Constant:
:$\map \det {\mathbf B^\intercal} = c \map \det {\mathbf A^\intercal}$
From from Determinant of Transpose:
:$\map \det {\mathbf B^\intercal} = \map \det {\mathbf B}$
:$\map \det {\mathbf A^\intercal} = \map \det {\mathbf A}$
and the result follows.
{{qed}}
Theorem: Determinant of Elementary Column Matrix/Exchange Columns

Let $e_3$ be the elementary column operation $\text {ECO} 3$:
{{begin-axiom}}
{{axiom | n = \text {ECO} 3
        | t = Exchange columns $i$ and $j$
        | m = \kappa_i \leftrightarrow \kappa_j
}}
{{end-axiom}}
which is to operate on some arbitrary matrix space.
Let $\mathbf E_3$ be the elementary column matrix corresponding to $e_3$.
The determinant of $\mathbf E_3$ is:
:$\map \det {\mathbf E_3} = -1$

Proof:
Let $\mathbf I$ denote the unit matrix of arbitrary order $n$.
By Determinant of Unit Matrix:
:$\map \det {\mathbf I} = 1$
Let $\rho$ be the permutation on $\tuple {1, 2, \ldots, n}$ which transposes $i$ and $j$.
From Parity of K-Cycle, $\map \sgn \rho = -1$.
By definition we have that $\mathbf E_3$ is $\mathbf I$ with columns $i$ and $j$ transposed.
By the definition of a determinant:
:$\ds \map \det {\mathbf I} = \sum_\lambda \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k k} }$
By Permutation of Determinant Indices:
:$\ds \map \det {\mathbf E_3} = \sum_\lambda \paren {\map \sgn \rho \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k \map \rho k} }$
We can take $\map \sgn \rho = -1$ outside the summation because it is constant, and so we get:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf E_3}
      | r = \map \sgn \rho \sum_\lambda \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k \map \rho k} }
      | c = 
}}
{{eqn | r = -\sum_\lambda \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \lambda k k} }
      | c = 
}}
{{eqn | r = -\map \det {\mathbf I}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sequence of Row Operations is Row Operation

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma_1$ be a row operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Let $\Gamma_2$ be a row operation which transforms $\mathbf B$ to another new matrix $\mathbf C \in \map \MM {m, n}$.
Then there exists another row operation $\Gamma$ which transforms $\mathbf A$ back to $\mathbf C$ such that $\Gamma$ consists of $\Gamma_1$ followed by $\Gamma_2$.

Proof:
Let $\sequence {e_i}_{1 \mathop \le i \mathop \le k}$ be the finite sequence of elementary row operations that compose $\Gamma_1$.
Let $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$ be the corresponding finite sequence of the elementary row matrices.
Let $\sequence {f_i}_{1 \mathop \le i \mathop \le l}$ be the finite sequence of elementary row operations that compose $\Gamma_2$.
Let $\sequence {\mathbf F_i}_{1 \mathop \le i \mathop \le l}$ be the corresponding finite sequence of the elementary row matrices.
From Row Operation is Equivalent to Pre-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf R_1 \mathbf A = \mathbf B$
where $\mathbf R$ is the product of $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$:
:$\mathbf R_1 = \mathbf E_k \mathbf E_{k - 1} \dotsb \mathbf E_2 \mathbf E_1$
Also from Row Operation is Equivalent to Pre-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf R_2 \mathbf B = \mathbf C$
where $\mathbf R_2$ is the product of $\sequence {\mathbf F_i}_{1 \mathop \le i \mathop \le l}$:
:$\mathbf R_2 = \mathbf F_l \mathbf F_{l - 1} \dotsb \mathbf F_2 \mathbf F_1$
Hence we have:
:$\mathbf R_2 \mathbf R_1 \mathbf A = \mathbf C$
where $\mathbf R := \mathbf R_2 \mathbf R_1$ is the product:
:$\mathbf F_l \mathbf F_{l - 1} \dotsb \mathbf F_2 \mathbf F_1 \mathbf E_k \mathbf E_{k - 1} \dotsb \mathbf E_2 \mathbf E_1$
Let $\Gamma$ be the row operation composed of the finite sequence of elementary row operations $\tuple {e_1, e_2, \ldots, e_{k - 1}, e_k, f_1, f_2, \ldots, f_{l - 1}, f_l}$.
Thus $\Gamma$ is a row operation which transforms $\mathbf A$ into $\mathbf C$.
Hence the result.
{{qed}}
Theorem: Sequence of Column Operations is Column Operation

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma_1$ be a column operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Let $\Gamma_2$ be a column operation which transforms $\mathbf B$ to another new matrix $\mathbf C \in \map \MM {m, n}$.
Then there exists another column operation $\Gamma$ which transforms $\mathbf A$ back to $\mathbf C$ such that $\Gamma$ consists of $\Gamma_1$ followed by $\Gamma_2$.

Proof:
Let $\sequence {e_i}_{1 \mathop \le i \mathop \le k}$ be the finite sequence of elementary column operations that compose $\Gamma_1$.
Let $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$ be the corresponding finite sequence of the elementary column matrices.
Let $\sequence {f_i}_{1 \mathop \le i \mathop \le l}$ be the finite sequence of elementary column operations that compose $\Gamma_2$.
Let $\sequence {\mathbf F_i}_{1 \mathop \le i \mathop \le l}$ be the corresponding finite sequence of the elementary column matrices.
From Column Operation is Equivalent to Post-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf A \mathbf R_1 = \mathbf B$
where $\mathbf R$ is the product of $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$:
:$\mathbf R_1 = \mathbf E_1 \mathbf E_2 \dotsb \mathbf E_{k - 1} \mathbf E_k$
Also from Column Operation is Equivalent to Post-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf B \mathbf R_2 = \mathbf C$
where $\mathbf R_2$ is the product of $\sequence {\mathbf F_i}_{1 \mathop \le i \mathop \le l}$:
:$\mathbf R_2 = \mathbf F_1 \mathbf F_2 \dotsb \mathbf F_{l - 1} \mathbf F_l$
Hence we have:
:$\mathbf A \mathbf R_1 \mathbf R_2 = \mathbf C$
where $\mathbf R := \mathbf R_1 \mathbf R_2$ is the product:
:$\mathbf E_1 \mathbf E_2 \dotsb \mathbf E_{k - 1} \mathbf E_k \mathbf F_1 \mathbf F_2 \dotsb \mathbf F_{l - 1} \mathbf F_l$
Let $\Gamma$ be the column operation composed of the finite sequence of elementary column operations $\tuple {e_1, e_2, \ldots, e_{k - 1}, e_k, f_1, f_2, \ldots, f_{l - 1}, f_l}$.
Thus $\Gamma$ is a column operation which transforms $\mathbf A$ into $\mathbf C$.
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Determinant

Let $\mathbf A = \sqbrk a_n$ be a square matrix of order $n$.
{{TFAE|def = Determinant of Matrix|view = the determinant of $\mathbf A$}}

Proof:
This is proved in Laplace Expansion Theorem for Determinants.
{{qed}}
Category:Determinants
32f91fz73q4e29hefegk5saeroae633
Theorem: Intersection With Singleton is Disjoint if Not Element

Let $S$ be a set.
Let $\set x$ be the singleton of $x$.
Then:
:$x \notin S$ {{iff}} $\set x \cap S = \O$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \set x \cap S = \O
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = \lnot \paren {y \in \set x \cap S}
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = \lnot \paren {y \in \set x \land y \in S}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = \lnot \paren {y \in \set x \land \lnot \lnot \paren {y \in S} }
      | c = Double Negation Introduction
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = y \in \set x \implies \lnot \paren {y \in S}
      | c = Conditional is Equivalent to Negation of Conjunction with Negative
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = y \in \set x \implies y \notin S
      | c = {{Defof|Element|Not Element}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall y
      | o =
      | r = y = x \implies y \notin S
      | c = {{Defof|Singleton}}
}}
{{eqn | ll= \leadstoandfrom
      | o =
      | r = x \notin S
      | c = {{Defof|Equality}}
}}
{{end-eqn}}
{{qed}}
Category:Singletons
Category:Disjoint Sets
oa4ozoro8hl8fdbbkduppgmrp3dkglz
Theorem: Determinant of Lower Triangular Matrix

Let $\mathbf T_n$ be a lower triangular matrix of order $n$.
Let $\map \det {\mathbf T_n}$ be the determinant of $\mathbf T_n$.
Then $\map \det {\mathbf T_n}$ is equal to the product of all the diagonal elements of $\mathbf T_n$.
That is:
:$\ds \map \det {\mathbf T_n} = \prod_{k \mathop = 1}^n a_{k k}$

Proof:
From Transpose of Upper Triangular Matrix is Lower Triangular, the transpose $\mathbf T_n^\intercal$ of $\mathbf T_n$ is an upper triangular matrix.
From Determinant of Upper Triangular Matrix, the determinant of $\mathbf T_n^\intercal$ is equal to the product of all the diagonal elements of $\mathbf T_n^\intercal$.
From Determinant of Transpose, the determinant of $\mathbf T_n^\intercal$ equals the determinant of $\mathbf T_n$.
Thus, because $\mathbf T_n$ and $\mathbf T_n^\intercal$ have the same diagonal elements, $\map \det {\mathbf T_n}$ is equal to the product of all the diagonal elements of $\mathbf T_n$.
{{qed}}
Theorem: Inverse of Matrix is Scalar Product of Adjugate by Reciprocal of Determinant

Let $\mathbf A = \sqbrk a_n$ be a nonsingular square matrix of order $n$.
Let $\map \det {\mathbf A}$ be the determinant of $\mathbf A$.
Let $\adj {\mathbf A}$ be the adjugate of $\mathbf A$.
Then:
:$\mathbf A^{-1} = \dfrac 1 {\map \det {\mathbf A} } \cdot \adj {\mathbf A}$
where $\mathbf A^{-1}$ denotes the inverse of $\mathbf A$

Proof:
Let $\mathbf I_n$ denote the unit matrix of order $n$.
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf A} \cdot \mathbf I_n
      | r = \mathbf A \cdot \adj {\mathbf A}
      | c = Matrix Product with Adjugate Matrix
}}
{{eqn | l = \map \det {\mathbf A} \cdot \mathbf A^{-1} \cdot \mathbf I_n
      | r = \mathbf A^{-1} \cdot \mathbf A \cdot \adj {\mathbf A}
}}
{{eqn | l = \map \det {\mathbf A} \cdot \mathbf A^{-1} \cdot \mathbf I_n
      | r = \mathbf I_n \cdot \adj {\mathbf A}
      | c = {{Defof|Inverse Matrix}}
}}
{{eqn | l = \map \det {\mathbf A} \cdot \mathbf A^{-1}
      | r = \adj {\mathbf A}
      | c = Unit Matrix is Identity for Matrix Multiplication
}}
{{eqn | l = \mathbf A^{-1}
      | r = \dfrac 1 {\map \det {\mathbf A} } \cdot \adj {\mathbf A}
}}
{{end-eqn}}
{{qed}}
Theorem: Greedy Algorithm yields Maximal Set

Let $\struct{S,\mathscr F}$ be an independence system.
Let $w : S \to \R_{\ge 0}$ be a weight function.
Then the Greedy Algorithm selects a maximal set $A_0$ in $\mathscr F$.

Proof:
{{ProofWanted}}
Category:Maximization Problem for Independence Systems
omhyyhdrmhuqurhcydk3z4mmkhrgbcg
Theorem: Greedy Algorithm may not yield Maximum Weight

Let $\struct {S,\mathscr F}$ be an independence system.
Let $w : S \to \R_{\ge 0}$ be a weight function.
Then the maximal set $A_0 \in \mathscr F$ selected by the Greedy Algorithm may not have maximum weight.

Proof:
{{ProofWanted}}
Category:Maximization Problem for Independence Systems
pvhcoq3lury3y2d5hshriio5ys2rn21
Theorem: Independent Subset is Contained in Base

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $\mathscr B$ denote the set of all bases of $M$.
Let $A \in \mathscr I$.
Then:
:$\exists B \in \mathscr B : A \subseteq B$

Proof:
Consider the ordered set $\struct {\mathscr I, \subseteq}$.
From Element of Finite Ordered Set is Between Maximal and Minimal Elements:
:$\exists B \in \mathscr I : A \subseteq B$ and $B$ is maximal in $\struct {\mathscr I, \subseteq}$.
By definition of a base:
:$B \in \mathscr B$
{{qed}}
Category:Matroid Independent Subsets
Category:Matroid Bases
gfu7b3gd5qj1dg81s8pceemn5hkhtgn
Theorem: Finite Non-Empty Subset of Ordered Set has Maximal and Minimal Elements/Corollary

Let $\struct {S, \preceq}$ be a finite ordered set.
Let $x \in S$.
Then there exists a maximal element $M \in S$ and a minimal element $m \in S$ such that:
:$m \preceq x \preceq M$

Proof:
Let $T = \set{y : x \preceq y}$.
By the reflexivity of the ordering $\preceq$:
:$x \preceq x$
So $x \in T$ and $T$ is non-empty.
From Finite Non-Empty Subset of Ordered Set has Maximal and Minimal Elements:
:$\struct {T, \preceq}$ has a maximal element $M \in T$
We now show that $M$ is a maximal element in $\struct{S, \preceq}$. 
Let $y \in S$ such that:
:$M \preceq y$
By the transitiviy of the ordering $\preceq$:
:$x \prec y$
So $y \in T$.
By the definition of a maximal element:
:$y = M$
Similarly for $T' = \set {y : y \preceq x}$:
:$\struct {T', \preceq}$ has a minimal element $m \in T'$
and $m$ is a minimal element in $\struct {S, \preceq}$.
{{qed}}
Category:Minimal Elements
Category:Maximal Elements
4q4bk1vp4vtrfpoodad23stgzy78baw
Theorem: Equivalent Conditions for Element is Loop

Let $M = \struct{S, \mathscr I}$ be a matroid.
Let $\sigma$ denote the closure operator on $M$.
Let $\rho$ denote the rank function of $M$.
Let $\mathscr B$ denote the set of all bases of $M$.
Let $x \in S$.
{{TFAE}}
:$(1)\quad x$ is a loop
:$(2)\quad x \in \map \sigma \O$ 
:$(3)\quad \map \rho {\set x} = 0$
:$(4)\quad \set x$ is a circuit
:$(5)\quad x$ is not an element of any $B \in \mathscr B$

Proof:
=== Condition $(1)$ iff Condition $(2)$ ===
Follows immediately from Element is Loop iff Member of Closure of Empty Set.
{{qed|lemma}}
Theorem: Power Set of Doubleton

Let $x, y$ be distinct objects.
Then the power set of the doubleton $\set {x, y}$ is:
:$\powerset {\set {x, y} } = \set {\O, \set x, \set y, \set {x, y} }$

Proof:
By definition of a subset:
:$\set x , \set y, \set {x, y} \subseteq \set {x, y}$
Let $A \subseteq \set {x, y}$:
:$A \ne \set x, \set y, \set {x, y}$
From set equality:
:$\set {x, y} \nsubseteq A$
From Doubleton of Elements is Subset:
:either $x \notin A$ or $y \notin A$.
{{WLOG}} assume that $x \notin A$.
From Intersection With Singleton is Disjoint if Not Element:
:$A \cap \set x = \O$
From Subset of Set Difference iff Disjoint Set:
:$A \subseteq \set {x, y} \setminus \set x$
From Set Difference of Doubleton and Singleton is Singleton:
:$A \subseteq \set y$
From set equality:
:$\set y \nsubseteq A$
From Singleton of Element is Subset:
:$y \notin A$.
From Intersection With Singleton is Disjoint if Not Element:
:$A \cap \set y = \O$
From Subset of Set Difference iff Disjoint Set:
:$A \subseteq \set y \setminus \set y$
From Set Difference with Self is Empty Set:
:$A \subseteq \O$
From Empty Set is Subset of All Sets:
:$\O \subseteq A$
From set equality:
:$A = \O$
It follows that:
:$\powerset {\set {x, y} } = \set {\O, \set x, \set y, \set {x, y} }$
{{qed}}
Category:Power Set
Category:Doubletons
qanzo2fnaw3r80r7pfy9mvbtwxv17e5
Theorem: Doubleton of Elements is Subset

Let $S$ be a set.
Let $\set {x,y}$ be the doubleton of distinct $x$ and $y$.
Then:
:$x, y \in S \iff \set {x,y} \subseteq S$

Proof:
=== Necessary Condition ===
Let $x, y \in S$.
From Singleton of Element is Subset:
:$\set x \subseteq S$
:$\set y \subseteq S$
From Union of Subsets is Subset:
:$\set x \cup \set y \subseteq S$
From Union of Disjoint Singletons is Doubleton:
: $\set x \cup \set y = \set {x, y}$
Hence:
:$\set {x,y} \subseteq S$
{{qed|lemma}}
Theorem: Sum of Unitary Divisors of Power of Prime

Let $n = p^k$ be the power of a prime number $p$.
Then the sum of all positive unitary divisors of $n$ is $1 + n$.

Proof:
Let $d \divides n$.
By Divisors of Power of Prime, $d = p^a$ for some positive integer $a \le k$.
We have $\dfrac n d = p^{k - a}$.
Suppose $d$ is a unitary divisor of $n$.
Then $d$ and $\dfrac n d$ are coprime.
If both $a, k - a \ne 0$, $p^a$ and $p^{k - a}$ have a common divisor: $p$.
Hence either $a = 0$ or $k - a = 0$.
This leads to $d = 1$ or $p^k$.
Hence the sum of all positive unitary divisors of $n$ is:
:$1 + p^k = 1 + n$
{{qed}}
Category:Prime Numbers
Category:Sum of Unitary Divisors
ebj0fv5t3kwe6rz3pfhvp8mk2uyf2lt