nyuuzyou/wikis huggingface dataset:
Bijection on Total Ordering reflects Total Ordering

== Theorem ==
Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $f: S \to T$ be a mapping to an arbitrary set $T$.
Let $\RR$ be a relation on $T$ defined such that:
:$\RR: = \set {\tuple {\map f x, \map f y}: x \preccurlyeq y}$
That is, $a$ is related to $b$ in $T$ they have preimages $x$ and $y$ under $f$ such that $x$ precedes $y$.
Then:
:$f$ is a bijection
:
:$\RR$ is a total ordering.
== Proof ==
=== Sufficient Condition ===
Let $f$ be a bijection.
Then $f$ is a fortiori a surjection.
Hence from Surjection on Total Ordering reflects Preordering it follows that $\RR$ is a preordering.
A total ordering is a preordering which is also antisymmetric and connected.
Hence it remains to be shown that:
:$\RR$ is antisymmetric
:$\RR$ is connected.
==== Antisymmetry ====
Let $a, b \in T$ such that:
:$a \mathrel \RR b$
:$b \mathrel \RR a$
Because $f$ is a surjection, it follows that:
:$\exists x \in S: a = \map f x$
:$\exists y \in S: b = \map f y$
Thus by definition of $\RR$:
:$x \preccurlyeq y$
:$y \preccurlyeq x$
But as $\preccurlyeq$ is an ordering, it is a fortiori antisymmetric.
That is:
:$x = y$
So:
:$\map f x = \map f y$
and so $a = b$.
Hence it follows that $\RR$ is antisymmetric.
==== Connectedness ====
Let $a, b \in T$.
Because $f$ is a surjection, it follows that:
:$\exists x \in S: a = \map f x$
:$\exists y \in S: b = \map f y$
Because $\preccurlyeq$ is an ordering, it is a fortiori connected.
That is, either:
:$x \preccurlyeq y$
or:
:$y \preccurlyeq x$
Hence by definition of $\RR$, either:
:$\map f x \mathrel \RR \map f y$
or:
:$\map f y \mathrel \RR \map f x$
That means either:
:$a \mathrel \RR b$
or:
:$b \mathrel \RR a$
As $a$ and $b$ were arbitrary, it follows that $\RR$ is connected.
Hence $\RR$ is a total ordering.
=== Necessary Condition ===
Let $\RR$ be a total ordering.
Then $\RR$ is a fortiori an ordering.
From Ordering is Preordering, $\RR$ is also a preordering.
From Surjection on Total Ordering reflects Preordering it follows that $f$ is a surjection.
It remains to be demonstrated that $f$ is an injection.
Let $x, y \in S$ such that $x \ne y$.
As $\preccurlyeq$ is an ordering, we have that $\preccurlyeq$ is a fortiori an antisymmetric relation.
Then either:
:$x \preccurlyeq y$
or:
:$y \preccurlyeq x$
but not both.
Hence by definition of $\RR$:
:$\map f x \mathrel \RR \map f y$
or:
:$\map f y \mathrel \RR \map f x$
but not both.
That is:
:$\map f x \ne \map f y$
and so by definition $f$ is an injection.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $41 \ \text {(c)}$
Category:Total Orderings
Category:Bijections
Bijective Continuous Linear Operator is not necessarily Invertible

== Theorem ==
Let $\struct {X, \norm {\, \cdot \,} }$ be the normed vector space.
Let $\map {CL} X := \map {CL} {X, X}$ be a continuous linear transformation space.
Let $I \in \map {CL} X$ be the identity element.
Suppose $A \in \map {CL} X$ is bijective.
Then $A$ is not necessarily invertible.
== Proof ==
Let $\mathbb F \in \set {\R, \C}$. 
Let $\map {c_{00} } {\mathbb F}$ be the space of almost-zero sequences on $\mathbb F$.
Let $\mathbf x = \tuple {x_1, x_2, \ldots, x_N, 0, \ldots} \in c_{00}$.
Let $A : c_{00} \to c_{00}$ be a mapping such that:
:$\map A {\tuple {x_1, x_2, x_3, \ldots} } = \tuple {x_1, \dfrac {x_2} 2, \dfrac{x_3} 3, \ldots}$
Let $\struct {\map {\ell^\infty} {\mathbb F}, \norm {\, \cdot \,}_\infty}$ be the normed vector space of bounded sequences on $\mathbb F$.
We have that Space of Almost-Zero Sequences is Subspace of Space of Bounded Sequences:
:$c_{00} \subseteq \ell^\infty$
Moreover, Space of Almost-Zero Sequences with Supremum Norm is Normed Vector Space.
=== $A$ is a linear operator ===
By definition, $A$ is a linear operator.
Let $\norm {\, \cdot \,}$ be the supremum operator norm.
=== $A$ is a continuous operator ===
By definition, $A$ is a diagonal operator with $\ds \sequence {\lambda_i}_{i \mathop \in \N_{> 0} } = \sequence {\frac 1 i}_{i \mathop \in \N_{> 0} }$.
By Supremum Operator Norm of Diagonal Operator over Bounded Sequence Space:
:$\ds \norm {A} = \sup_{i \mathop \in \N_{> 0} } \size {\lambda_i}$
Then:
By Continuity of Linear Transformation between Normed Vector Spaces, $A$ is continuous.
=== $A$ is an injection ===
Suppose:
:$\forall \mathbf x, y \in \ell^\infty : \map A {\mathbf x} = \map A {\mathbf y}$.
Then:
By definition, $A$ is injective.
=== $A$ is a surjection ===
Let $\mathbf y \in c_{00}$ and $N \in \N_{> 0}$ such that:
:$\forall i \in \N_{> 0} : \paren {i \le N \implies y_i \in \R} \land \paren {i > N \implies \paren {y_i = 0} }$
Also, Real Multiplication is Closed.
Then:
:$\exists \mathbf x \in c_{00} : \forall i \in \N_{> 0} : \paren {i \le N \implies \paren {x_i = i \cdot y_i \in \R} } \land \paren {i > N \implies \paren {x_i = 0} }$
Hence:
By definition, $A$ is surjective.
By definition, $A$ is bijective.
=== $A$ is not invertible ===
 there is $B \in \map {CL} {c_{00}}$ which is the inverse of $A$.
Let $\mathbf e_m = \tuple {\underbrace{0, \ldots, 0}_{m - 1}, 1, 0, \ldots}$.
Then:
However, by definition of supremum operator norm:
:$\norm B = \map \sup {\norm {\map B {\mathbf x} }_\infty : \mathbf x \in c_{00}, \norm {\mathbf x}_\infty \le 1}$
where $\norm {\map B {\mathbf x} }_\infty \in \R$.
This is a contradiction.
Hence, $A$ is bijective, but not invertible.
== Sources ==
* : Chapter $\S 2.4$: Composition of continuous linear transformations
Category:Continuous Linear Transformations
Category:Bijections
Category:Inverse Mappings
Bijective Relation has Left and Right Inverse

== Theorem ==
Let $\RR \subseteq S \times T$ be a relation on a cartesian product $S \times T$.
Let:
:$I_S$ be the identity mapping on $S$
:$I_T$ be the identity mapping on $T$.
Let $\RR^{-1}$ be the inverse relation of $\RR$.
Let $\RR$ be a bijection.
Then:
:$\RR^{-1} \circ \RR = I_S$
and
:$\RR \circ \RR^{-1} = I_T$
where $\circ$ denotes composition of relations.
== Proof ==
Suppose $\RR$ is a bijection.
Then by definition:
:$(1): \quad \RR$ is a surjection and therefore right-total.
:$(2): \quad \RR$ is a mapping and therefore left-total.
:$(3): \quad \RR$ is a one-to-one relation and therefore also both a many-to-one relation and a one-to-many relation.
By Inverses of Right-Total and Left-Total Relations, we have that $\RR^{-1}$ is also both right-total and left-total.
By Inverse of Many-to-One Relation is One-to-Many we have that $\RR^{-1}$ is also both a many-to-one relation and a one-to-many relation.
From Condition for Composite Relation with Inverse to be Identity, it follows that:
:$\RR^{-1} \circ \RR = I_S$
and:
:$\RR \circ \RR^{-1} = I_T$
Hence the result.
== Sources ==
* : Chapter $\text I$: Algebraic Structures: $\S 5$: Composites and Inverses of Functions: Exercise $5.8 \ \text{(f)}$
Category:Inverse Relations
Category:Bijections
Bijective Restriction/Examples/x^2-4x+5

== Example of Bijective Restrictions ==
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = x^2 - 4 x + 5$
The following real functions are bijective restrictions of $f$:
== Proof ==
From Image of $\map f x = x^2 - 4 x + 5$, the image of $f$ is given by:
:$\Img f = \hointr 1 \to$
Thus a surjective restriction of $f$ can be found as:
:$g: \R \to \hointr 1 \to: \map g x = x^2 - 4 x + 5$
It remains to show that $f_1$ and $f_2$ are injective.
It is established in Image of $\map f x = x^2 - 4 x + 5$ that $f$ has a minimum at $x = 2$.
As this is the only stationary point of $f$, it follows that:
:$\map f x$ is strictly decreasing on $\hointl \gets 2$
:$\map f x$ is strictly increasing on $\hointl 2 \to$
From Strictly Monotone Mapping with Totally Ordered Domain is Injective it follows that both $f_1$ and $f_2$ are injections.
Hence, by definition, $f_1$ and $f_2$ are bijective restrictions of $f$.
== Sources ==
* : Chapter $4$: Mappings: Exercise $12 \ \text{(iii)}$
Category:Examples of Bijective Restrictions
Bilinear Form (Polynomial Theory)/Examples/Arbitrary Example 2

== Example of Bilinear Form ==
Let $\set {x_1, x_2, \ldots, x_n}$ and $\set {y_1, y_2, \ldots, y_n}$ be sets of variables.
The expression:
is a bilinear form of order $2$ $\set {x_1, x_2, \ldots, x_n}$ and $\set {y_1, y_2, \ldots, y_n}$.
== Sources ==
* 
* 
Category:Examples of Bilinear Forms (Polynomial Theory)
Bilinear Form is Reflexive iff Symmetric or Alternating

== Theorem ==
Let $\mathbb K$ be a field.
Let $V$ be a vector space over $\mathbb K$.
Let $b$ be a bilinear form on $V$.
Then the following are equivalent:
:$(1): \quad$ $b$ is reflexive
:$(2): \quad$ $b$ is symmetric or alternating
== Proof ==
=== 1 implies 2 ===
Follows from Reflexive Bilinear Form is Symmetric or Alternating
=== 2 implies 1 ===
Follows from:
:Symmetric Bilinear Form is Reflexive
:Alternating Bilinear Form is Reflexive
Category:Bilinear Forms (Linear Algebra)
Bill's Family

== Problem ==
Bill, in his middle-age, marries a young lady but divorces her soon after.
Bill's son marries the young lady's mother.
What is:
:$(\text a): \quad$ Bill's relationship with the young lady's mother?
:$(\text b): \quad$ Bill's relationship with his former wife?
== Solution ==
Bill is simultaneously:
:$(\text a): \quad$ the father-in-law of his ex-mother-in-law
and:
:$(\text b): \quad$ the stepgrandfather of his former wife.
Category:Strange Family Problems
Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union

== Theorem ==
Let $S$ and $T$ be sets.
Let $S \times T$ be the Cartesian product of $S$ and $T$ realized as a set of ordered pairs in Kuratowski formalization.
Then $S \times T \subseteq \powerset {\powerset {S \cup T} }$.
== Proof 1 ==
== Proof 2 ==
Category:Cartesian Product
Category:Power Set
Category:Set Union
Category:Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union
Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union/Proof 1

== Theorem ==
== Proof ==
Let $x \in S$ and $y \in T$.
We are to show that $\set {\set x, \set {x, y} } \in \powerset {\powerset {S \cup T} }$.
Category:Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union
Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union/Proof 2

== Theorem ==
== Proof ==
By Law of Excluded Middle there are two choices:
:$S \times T = \O$
:$S \times T \ne \O$
Suppose $S \times T = \O$.
By Empty Set is Subset of Power Set:
:$S \times T \subseteq \powerset {\powerset {S \cup T} }$
Suppose $S \times T \ne \O$.
By Cartesian Product is Empty iff Factor is Empty, there exist $x$ and $y$ such that:
:$x \in S$
:$y \in T$
Let us express the ordered pair $\tuple {x, y}$ using the Kuratowski formalization:
:$\tuple {x, y} \equiv \set { \set x, \set {x, y} }$
We now show that:
:$\set {\set x, \set {x, y} } \in \powerset {\powerset {S \cup T} }$
Indeed:
Category:Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union
Binary Coproduct in Preadditive Category is Biproduct

== Theorem ==
Let $A$ be a preadditive category.
Let $a_1, a_2$ be objects of $A$.
Let $(a_1 \sqcup a_2, i_1, i_2)$ be their binary coproduct, assuming it exists.
Let $p_1 : a_1 \sqcup a_2 \to a_1$ be the unique morphism with:
:$p_1 \circ i_1 = 1 : a_1 \to a_1$
:$p_1 \circ i_2 = 0 : a_1 \to a_2$
Let $p_2 : a_1 \sqcup a_2 \to a_2$ be the unique morphism with:
:$p_2 \circ i_1 = 0 : a_2 \to a_1$
:$p_2 \circ i_2 = 1 : a_2 \to a_2$
where $1$ is the identity morphism and $0$ is the zero morphism.
Then $(a_1 \sqcup a_2, i_1, i_2, p_1, p_2)$ is the binary biproduct of $a_1$ and $a_2$.
== Proof ==
By definition of binary biproduct, it remains to verify that:
:$i_1\circ p_1 + i_2 \circ p_2 = 1 : a_1 \sqcup a_2 \to a_1 \sqcup a_2$.
By definition of binary coproduct and identity morphism, $1 : a_1 \sqcup a_2 \to a_1 \sqcup a_2$ is the unique morphism with:
:$1 \circ i_1 = i_1$
:$1 \circ i_2 = i_2$
Thus it remains to verify that $i_1\circ p_1 + i_2 \circ p_2$ satisfies the same condition:
== Also see ==
* Binary Product in Preadditive Category is Biproduct
Category:Preadditive Categories
Binary Logarithm/Examples/10

== Example of Binary Logarithm ==
The binary logarithm of $10$ is:
:$\log_2 10 \approx 3 \cdotp 32192 \, 80948 \, 87362 \, 34787 \, 0319 \ldots$
== Sources ==
* : $3 \cdotp 321 \, 928 \ldots$
* : $3 \cdotp 32192 \, 8 \ldots$
Category:Examples of Binary Logarithms
Binary Logical Connective is Self-Inverse iff Exclusive Or

== Source Work ==
:
: Chapter $2$: Propositional Calculus
:: $2.1$. Boolean Operations
== Mistake ==
Let $\circ$ be a binary logical connective.
Then:
:$\paren {p \circ q} \circ q \dashv \vdash p$
 $\circ$ is the exclusive or operator.
:$\mathsf{XOR}$ is also essential since it is the only operator having an inverse, namely itself
::$\paren {p \oplus q} \oplus q = p$''
Incorrect, as the biconditional operator has the same properties:
:$\paren {\paren {p \iff q} \iff q} = p$
== Proof ==
See Binary Logical Connectives with Inverse.
== Sources ==
* : Chapter $2$: Propositional Calculus: $\S 2.1$: Boolean operators
Category:Mistakes/Mathematical Logic for Computer Science
Binary Notation/Examples

== Examples of Binary Notation ==
=== $13$ in Binary Notation ===
=== $19$ in Binary Notation ===
=== $23$ in Binary Notation ===
=== $36$ in Binary Notation ===
=== $47$ in Binary Notation ===
=== $68$ in Binary Notation ===
=== $127$ in Binary Notation ===
Category:Examples of Binary Notation
Binary Operation on Subset is Binary Operation

== Theorem ==
Let $S$ be a set.
Let $\circ$ be a binary operation on $S$.
Let $T \subseteq S$.
Let $\circ {\restriction}_T$ be the restriction of $\circ$ to $T$.
Then $\circ {\restriction}_T$ is a binary operation on $T$.
== Proof ==
Let $\Bbb U$ be a universal set.
Let $\circ: S \times S \to \Bbb U$ be a binary operation on $S$.
Let $T \subseteq S$.
Let $\tuple {a, b} \in T \times T$.
By definition of ordered pair and cartesian product:
:$a \in T$ and $b \in T$
As $T \subseteq S$, it follows that:
:$a \in S$ and $b \in S$
Thus:
:$\tuple {a, b} \in S \times S$
As $\circ$ is a binary operation on $S$, it follows that:
:$\map \circ {a, b} \in \Bbb U$
But by definition of restriction of $\circ$:
:$\map \circ {a, b} = \map {\circ {\restriction}_T} {a, b}$
Thus:
:$\map {\circ {\restriction}_T} {a, b} \in \Bbb U$
As $a$ and $b$ are arbitrary elements of $T$, it follows that this holds for all $a, b \in T$.
Hence the result by definition of binary operation.
Category:Operations
Binary Product as Limit

== Theorem ==
Let $\mathbf C$ be a metacategory.
Let $C_1, C_2$ be objects of $\mathbf C$.
Let their binary product $C_1 \times C_2$ exist in $\mathbf C$.
Then $C_1 \times C_2$ is the limit of the diagram $D: 2 \to \mathbf C$ defined by:
:$D_0 := C_1, D_1 := C_2$
where $2$ is the discrete category with two objects $0, 1$.
== Proof ==
Since there are no non-identity morphisms, a cone to $D$ is simply a pair:
::$\begin{xy}\xymatrix@+1em@L+3px{
 C_1
&
 C
 \ar[l]_*+{f_1}
 \ar[r]^*+{f_2}
&
 C_2
}\end{xy}$
of morphisms with common domain $C$.
By the UMP of the binary product $C_1 \times C_2$, for such a cone to $D$ there is a unique $u: C \to C_1 \times C_2$ making:
::$\begin{xy}\xymatrix@L+3px@+1em{
&
 C
 \ar[dl]_*+{f_1}
 \ar@{-->}[d]^*{u}
 \ar[dr]^*+{f_2}
\\
 C_1
&
 C_1 \times C_2
 \ar[l]_*+{p_1}
 \ar[r]^*+{p_2}
&
 C_2
}\end{xy}$
a commutative diagram.
The conditions $p_1 \circ u = f_1$ and $p_2 \circ u = f_2$ precisely mean that $u: C \to C_1 \times C_2$ is a morphism of cones.
Thus for every cone $\struct{C, f_1, f_2}$ to $D$, there is a unique morphism of cones to the cone $\struct{C_1 \times C_2, p_1, p_2}$.
That is, $\struct{C_1 \times C_2, p_1, p_2}$ is a terminal object in $\map {\mathbf{Cone}} D$, the category of cones to $D$.
Hence the result, by definition of limit.
== Sources ==
* : $\S 5.4$: Example $5.17$
Category:Category Theory
Binary Product in Preadditive Category is Biproduct

== Theorem ==
Let $A$ be a preadditive category.
Let $a_1, a_2$ be objects of $A$.
Let $(a_1 \times a_2, p_1, p_2)$ be their binary product, assuming it exists.
Let $i_1 : a_1 \to a_1 \times a_2$ be the unique morphism with:
:$p_1 \circ i_1 = 1 : a_1 \to a_1$
:$p_2 \circ i_1 = 0 : a_1 \to a_2$
Let $i_2 : a_1 \to a_1 \times a_2$ be the unique morphism with:
:$p_1 \circ i_2 = 0 : a_2 \to a_1$
:$p_2 \circ i_2 = 1 : a_2 \to a_2$
where $1$ is the identity morphism and $0$ is the zero morphism.
Then $(a_1 \times a_2, i_1, i_2, p_1, p_2)$ is the binary biproduct of $a_1$ and $a_2$.
== Proof ==
By definition of binary biproduct, it remains to verify that:
:$i_1\circ p_1 + i_2 \circ p_2 = 1 : a_1 \times a_2 \to a_1 \times a_2$.
By definition of binary product and identity morphism, $1 : a_1 \times a_2 \to a_1 \times a_2$ is the unique morphism with:
:$p_1 \circ 1 = p_1$
:$p_2 \circ 1 = p_2$
Thus it remains to verify that $i_1\circ p_1 + i_2 \circ p_2$ satisfies the same condition:
== Also see ==
* Binary Coproduct in Preadditive Category is Biproduct
Category:Preadditive Categories
Binary Relation is Subclass of Product of Domain with Range

== Theorem ==
Let $V$ be a basic universe.
Let $\RR \subseteq V \times V$ be a relation.
Let $\Dom \RR$ denote the domain of $\RR$.
Let $\Img \RR$ denote the image of $\RR$.
Then:
:$\RR$ is a subclass of $\Dom \RR \times \Img \RR$
== Proof ==
Let $\tuple {x, y} \in \RR$.
Then by definition of domain of $\RR$:
:$x \in \Dom \RR$
and by definition of image of $\RR$:
:$y \in \Img \RR$
Hence by definition of Cartesian product:
:$\tuple {x, y} \in \Dom \RR \times \Img \RR$
Hence the result by definition of subclass:
:$\RR \subseteq \paren {\Dom \RR \times \Img \RR}$
== Sources ==
* : Chapter $2$: Some Basics of Class-Set Theory: $\S 8$ Relations
Category:Relation Theory
Binary Sequence Codes are Primitive Recursive

== Theorem ==
The following function is primitive recursive:
:$\map {\operatorname{bincode} } {n, i} = o_i$
where $o_i$ is the number of $1$ digits between the $i - 1$-th and $i$-th $0$ digit in the base-$2$ representation of $n$, starting from the least significant digits.
As a special case, $\map {\operatorname{bincode} } {n, 0}$ is the number of $1$ digits before the first $0$ digit.
In other words, suppose the base-$2$ representation of $n$ is:
:$\sqbrk {\dots 1 1 \dots 1 1 0 1 1 \dots 1 1 0 1 1 \dots 1 1}$
Then $\map {\operatorname{bincode} } {n, i}$ is the length of the $i + 1$-th string of $1$ digits, counting from the right.
== Proof ==
By Basis Representation is Primitive Recursive, we have that $\map {\operatorname{basis} } {b, n, i}$ is primitive recursive.
Consider the function:
:$\map z {n, i} = \begin{cases}
\map {\mu j < n} {\map {\operatorname{basis} } {2, n, j} = 0} & : i = 0 \\
\map {\mu j < n} {j > \map z {n, i - 1} \land \map {\operatorname{basis} } {2, n, j} = 0} & : i > 0
\end{cases}$
It returns the position of the $i + 1$-th $0$ in the base-$2$ representation of $n$.
If the digit exists, it will always be found, as the base-$2$ representation is never longer than $n$.
If there is no such digit, then it returns a position beyond the representation.
In particular, consecutive values of $z$ that are beyond its length will always be at most $1$ apart, and increasing.
Additionally $z$, is primitive recursive, as:
* Constant Function is Primitive Recursive
* Equality Relation is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Bounded Minimization is Primitive Recursive
and it is obtained by primitive recursion on them.
Then:
:$\map {\operatorname{bincode} } {n, i} = \begin{cases}
\map z {n, 0} & : i = 0 \\
\map z {n, i} - \map z {n, i - 1} - 1 & : i > 0
\end{cases}$
which is primitive recursive by:
* Definition by Cases is Primitive Recursive
* Cut-Off Subtraction is Primitive Recursive
in addition to the above.
Category:Primitive Recursive Functions
Binary Truth Functions

== Theorem ==
There are $16$ distinct binary truth functions:
* Two constant operations:
** $\map {f_\F} {p, q} = \F$
** $\map {f_\T} {p, q} = \T$
* Two projections:
** $\map {\pr_1} {p, q} = p$
** $\map {\pr_2} {p, q} = q$
* Two negated projections:
** $\map {\overline {\pr_1} } {p, q} = \neg p$
** $\map {\overline {\pr_2} } {p, q} = \neg q$
* The conjunction: $p \land q$
* The disjunction: $p \lor q$
* Two conditionals:
** $p \implies q$
** $q \implies p$
* The biconditional: $p \iff q$
* The exclusive or: $\map \neg {p \iff q}$
* Two negated conditionals:
** $\map \neg {p \implies q}$
** $\map \neg {q \implies p}$
* The NAND: $p \uparrow q$
* The NOR: $p \downarrow q$
== Proof ==
From Count of Truth Functions there are $2^{\paren {2^2} } = 16$ distinct truth functions on $2$ variables.
These can be depicted in a truth table as follows:
$\begin{array}{|r|cccc|} \hline
p & \T & \T & \F & \F \\
q & \T & \F & \T & \F \\
\hline
\map {f_\T} {p, q} & \T & \T & \T & \T \\
p \lor q & \T & \T & \T & \F \\
p \impliedby q & \T & \T & \F & \T \\
\map {\pr_1} {p, q} & \T & \T & \F & \F \\
p \implies q & \T & \F & \T & \T \\
\map {\pr_2} {p, q} & \T & \F & \T & \F \\
p \iff q & \T & \F & \F & \T \\
p \land q & \T & \F & \F & \F \\
p \uparrow q & \F & \T & \T & \T \\
\map \neg {p \iff q} & \F & \T & \T & \F \\
\map {\overline {\pr_2} } {p, q} & \F & \T & \F & \T \\
\map \neg {p \implies q} & \F & \T & \F & \F \\
\map {\overline {\pr_1} } {p, q} & \F & \F & \T & \T \\
\map \neg {p \impliedby q} & \F & \F & \T & \F \\
p \downarrow q & \F & \F & \F & \T \\
\map {f_\F} {p, q} & \F & \F & \F & \F \\
\hline
\end{array}$
That accounts for all $16$ of them.
== Sources ==
* : $\S 2.5$: Further Logical Constants
* : Chapter $2$: The Propositional Calculus $2$: $3$ Truth-Tables
* : Chapter $2$: Propositional Calculus: $\S 2.1$: Boolean operators
* : $\S 2.4.1$: Figure $2.5$
Category:Truth Functions
Binding Constraint/Examples/x^2 + y^2 le 2

== Example of Binding Constraint ==
Consider the weak inequality:
:$x^2 + y^2 \le 2$
Consider the point $\tuple {x, y} = \tuple {1, 1}$.
Then the constraint $x^2 + y^2 \le 2$ is binding at $\tuple {1, 1}$, as $1^2 + 1^2 = 2$.
== Sources ==
* 
Category:Examples of Binding Constraints
Binding Constraint/Examples/y + 2x ge 13

== Example of Binding Constraint ==
Consider the weak inequality:
:$y + 2 x \ge 13$
This is a binding constraint at $\tuple {6, 1}$ and $\tuple {0, 13}$, for example, as:
:$1 + 2 \times 6 = 13$
:$13 + 2 \times 0 = 13$
== Sources ==
* 
* 
Category:Examples of Binding Constraints
Binding Priority/Examples/Conjunction over Conditional

== Example of Binding Priority ==
The convention for binding priority states that:
:$\paren {x < y \land y < z} \implies x < z$
can be written as:
:$x < y \land y < z \implies x < z$
as $\land$ has a higher binding priority than $\implies$.
== Sources ==
* : $\S 1.2$ Logic and Notation: $(3)$
Category:Examples of Binding Priority
Binding Priority/Examples/Disjunction over Biconditional

== Example of Binding Priority ==
The convention for binding priority states that:
:$x + y \ne 0 \iff \paren {x \ne 0 \lor y \ne 0}$
can be written as:
:$x + y \ne 0 \iff x \ne 0 \lor y \ne 0$
as $\lor$ has a higher binding priority than $\iff$.
== Sources ==
* : $\S 1.2$ Logic and Notation
Category:Examples of Binding Priority
Binet's Formula for Logarithm of Gamma Function/Formulation 1

== Theorem == 
Let $z$ be a complex number with a strictly positive real part.
Then: 
:$\ds \Ln \map \Gamma z = \paren {z - \frac 1 2} \Ln z - z + \frac 1 2 \ln 2 \pi + \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t z} } t \rd t$
where: 
:$\Gamma$ is the Gamma function
:$\Ln$ is the principal branch of the complex logarithm. 
=== Corollary ===
== Proof == 
We have:
Setting $z:= \dfrac 1 2$, we obtain:
Let:
:$\ds J = \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t/2} } t \rd t$
:$\ds I = \int_0^\infty \paren {\frac 1 2 - \frac 1 t + \frac 1 {e^t - 1} } \frac {e^{-t} } t \rd t$
Then our last equation becomes:
:$\ds \frac 1 2 \map \Ln {\pi } = \dfrac 1 2 + J - I$
Setting $t:= \dfrac 1 2 u$ and $\rd t = \dfrac 1 2 \rd u$ we can rewrite $I$ as:
Therefore, taking the difference of $J$ and $I$, we obtain:
Solving for $J$, we obtain:
Therefore:
Therefore:
== Sources == 
* : $12.31$: Binet's first expression for $\log \Gamma \paren z$ in terms of an infinite integral
Category:Binet's Formula for Logarithm of Gamma Function