nyuuzyou/wikis huggingface dataset:
Long Period Prime/Sequence

== Sequence ==
The sequence of long period primes begins:
:$7$, $17$, $19$, $23$, $29$, $47$, $59$, $61$, $97$, $109$, $113$, $131$, $149$, $167$, $179$, $\ldots$
== Proof ==
Demonstrated by inspection and calculation.
From Reciprocals of Prime Numbers:
Category:Long Period Primes
Long Radius of Regular Polygon equals Radius of Circumcircle

== Theorem ==
Let $P$ be a regular polygon.
Let $C$ be the circumcircle of $P$.
The long radius of $P$ is equal to the radius of $C$.
== Proof ==
By definition of circumcircle, $C$ is the circle such that all vertices of $P$ are on $C$.
By definition, the center of $P$ is defined as the center of $C$.
Hence:
:$OA$ is the radius of $C$
and also:
:$OA$ is the long radius of $P$.
Hence the result.
== Sources ==
* 
* 
Category:Regular Polygons
Longest Sequence of Consecutive Primes in Arithmetic Sequence

== Sequence ==
The longest known sequence of consecutive prime numbers in arithmetic sequence starts at $121 \, 174 \, 811$, has a length of $6$ and a common difference of $30$:
:$121 \, 174 \, 811, 121 \, 174 \, 841, 121 \, 174 \, 871, 121 \, 174 \, 901, 121 \, 174 \, 931, 121 \, 174 \, 961$
== Proof ==
But note that $121 \, 174 \, 811 + 6 \times 30 = 121 \, 174 \, 991 = 7^2 \times 2 \, 472 \, 959$ and so is not prime.
Inspection of tables of primes (or a computer search) will reveal that no longer such sequences are known.
== Sources ==
* 
* : $121,174,811$
Category:Prime Numbers
Category:Arithmetic Sequences
Longitudes on Mercator's Projection are Same Distance Apart

== Theorem ==
Let $\MM$ be a Mercator's projection of Earth's surface such that the cylinder circumscribing Earth intersects it along the equator.
Then equally spaced lines of longitude on Earth map to parallel lines on $\MM$ which are also equally spaced.
== Proof ==
== Sources ==
* 
* 
Category:Mercator's Projection
Category:Longitude
Loop-Digraph as a Relation

== Theorem ==
A loop-digraph is the same thing as a relational structure.
== Proof ==
A loop-digraph is a graph such that:
:it is not necessarily antireflexive
:it is not necessarily symmetric.
Hence a loop-digraph is an ordered pair:
:$G = \struct {V, E}$
such that:
:$V$ is a set of objects
:$E$ is a relation on $V$.
This defines a relational structure.
== Sources ==
* : Chapter $1$: Mathematical Models: $\S 1.6$: Networks as Mathematical Models: Problem $42$
Category:Loop-Digraphs
Category:Relation Theory
Loop Belongs to Every Flat

== Theorem ==
Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $A \subseteq S$.
Let $x \in S$.
If $x$ is a loop and $A$ is a flat subset then $x \in A$.
== Proof ==
Let $\rho: \powerset S \to \Z$ denote the rank function of $M$.
We proceed by Proof by Contraposition.
That is, it is shown that:
:if $x \notin A$ then either $x$ is not a loop or $A$ is not a flat subset
Let $x \notin A$.
Let $x$ be a loop.
By definition of a loop:
:$\set x$ is a dependent subset.
From Rank Function is Increasing:
:$\map \rho A \le \map \rho {A \cup \set x}$
Let $X \in \mathscr I$ such that $X \subseteq A \cup \set x$.
From Superset of Dependent Set is Dependent:
:$\set x \nsubseteq X$
From Singleton of Element is Subset:
:$x \notin X$
So:
:$X \subseteq A$
By definition of the rank function:
:$\size X \le \map \rho A$
From Max Operation Yields Supremum of Parameters:
:$\map \rho {A \cup \set x} = \max \set{\size X : X \in \mathscr I \land X \subseteq A \cup \set x} \le \map \rho A$
Then:
:$\map \rho A = \map \rho {A \cup \set x}$
If follows that $A$ is not a flat subset by definition.
It has been shown that:
:if $x \notin A$ then either $x$ is not a loop or $A$ is not a flat subset
The theorem holds by the Rule of Transposition.
== Sources ==
* Chapter $1.$ $\S 4.$ Loops and parallel elements
Category:Matroid Loops
Category:Matroid Flats
Lord Dunsany's Chess Problem

== Problem ==
== Solution ==
It is first noted that the black queen is on a white square.
But according to the starting position, the queen starts on her own colour.
That means the black queen and king are not where they started.
The only way for that to happen is if at least one of the black pawns has been moved.
But pawns cannot go backwards.
So the only way the position is legal is if the board is such that black is at the bottom playing up, and white is at the top playing down.
Hence none of the black pawns, being on the $7$th rank, are able to move at this time.
With that in mind, the game progresses as follows.
Note that although the board has been turned round, the ranks and files remain labelled as they are in the diagram, in order to limit confusion.
White moves:
:$(1): \quad \text N \text g 1 - \text e 2$
Suppose black now moves:
:$(1): \quad \ldots \qquad \text N \text b 8 - \text a 6$:
White moves:
:$(2): \quad \text N \text e 2 - \text d 4$:
and whatever black does, white then moves either to $\text N \text d 4 - \text c 6$ or $\text N \text d 4 - \text e 6$ mate.
Now suppose black moves:
:$(1): \quad \ldots \qquad \text N \text b 8 - \text c 6$:
White moves:
:$(2): \quad \text N \text e 2 - \text f 4$:
threatening mate next move by $\text N \text f 4 - \text e 6$.
To prevent that, black can delay the inevitable by playing:
:$(2): \quad \ldots \quad \text N \text c 6 - \text d 4$:
which of course is immediately countered by: 
:$(3): \quad \text Q \times N$:
and there is nothing black can do to prevent:
:$(4): \quad \text N \text f 4 - \text e 6$ mate
It is worth noting that on move $(2)$, black could play $\text b 7 - \text b 8 (\text Q)$, but by then it is too late to get that new queen out before the hammer blow.
If we explore the possibility of black moving the knight on $\text g 8$, we see that it cannot get itself into position to threaten white's knight in time to prevent the mate in $3$.
== Historical Note ==
== Sources ==
* : $14$. Nine More Problems: $3$
Category:Chess Problems
Lorentz Transformation/Examples/Arbitrary Example 1

== Example of Lorentz Transformation ==
The following equations are examples of those used for a Lorentz transformation:
where:
:$\beta = \dfrac 1 {\sqrt {1 - \dfrac {v^2} {c^2} } }$
:$v$ denotes the magnitude of the relative velocity of the two frames of reference.
== Sources ==
* 
* 
Category:Examples of Lorentz Transformations
Lower Adjoint Preserves All Suprema

== Theorem ==
Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.
Let $d: T \to S$ be an lower adjoint of Galois connection.
Then $d$ preserves all suprema.
== Proof ==
By definition of lower adjoint
:$\exists g: S \to T: \left({g, d}\right)$ is a Galois connection
Let $X$ be a subset of $T$ such that
:$X$ admits a supremum.
We will prove as lemma 1 that
:$\forall s \in S: s$ is upper bound for $d^\to\left({X}\right) \implies d\left({\sup X}\right) \preceq s$
Let $s \in S$ such that
:$s$ is upper bound for $d^\to\left({X}\right)$
We will prove as sublemma that
:$g\left({s}\right)$ is upper bound for $X$
Let $t \in X$.
By definition of image of set:
:$d \left({t})\right) \in d^\to \left({X}\right)$
By definition of upper bound:
:$d\left({t}\right) \preceq s$
Thus by definition of Galois connection:
:$t \precsim g\left({s}\right)$
This ends the proof of sublemma.
By definition of supremum:
:$\sup X \precsim g\left({t}\right)$
Thus by definition of Galois connection:
:$d\left({\sup X}\right) \preceq t$
This ends the proof of lemma 1.
We will prove as lemma 2 that
:$d\left({\sup X}\right)$ is upper bound for $d^\to\left({X}\right)$
Let $s \in d^\to\left({X}\right)$.
By definition of image of set:
:$\exists t \in T: t \in X \land d\left({t}\right) = s$
By definition of supremum:
:$\sup X$ is upper bound for $X$
By definition of upper bound:
:$t \precsim \sup X$
By definition of Galois connection:
:$d$ is increasing mapping.
Thus by definition of increasing mapping:
:$s \preceq d\left({\sup X}\right)$
This ends the proof of lemma 2.
Thus by definition of supremum:
:$d^\to\left({X}\right)$ admits a supremum
and
:$\sup\left({d^\to\left({X}\right)}\right) = d\left({\sup X}\right)$
Thus by definition:
:$g$ preserves supremum on $X$
Thus by definition:
:$g$ preserves all suprema.
== Sources ==
* 
* 
Category:Galois Connections
Lower Adjoint at Element is Minimum of Preimage of Singleton of Element implies Composition is Identity

== Theorem ==
Let $L = \struct {S, \preceq}, R = \struct {T, \precsim}$ be ordered sets.
Let $g: S \to T, d: T \to S$ be mappings such that
:$\forall t \in T: \map d t = \min \set {g^{-1} \sqbrk {\set t} }$
Then $g \circ d = I_T$
where $I_T$ denotes the identity mapping of $T$.
== Proof ==
Let $t \in T$.
By assumption:
:$\map d t = \min \set {g^{-1} \sqbrk {\set t} }$
By definition of min operation:
:$\map d t = \map \inf {g^{-1} \sqbrk {\set t} }$ and $\map d t \in g^{-1} \sqbrk {\set t}$
By definition of image of set:
:$\map g {\map d t} \in \set t$
By definition of singleton:
:$\map g {\map d t} = t$
Thus by definition of composition of mappings:
:$\map {\paren {g \circ d} } t = t$
== Sources ==
* 
Category:Galois Connections
Lower Bound for Binomial Coefficient

== Theorem ==
Let $n, k \in \Z$ such that $n \ge k \ge 0$.
Then:
:$\dbinom n k \ge \paren {\dfrac {\paren {n - k} e} k}^k \dfrac 1 {e k}$
where $\dbinom n k$ denotes a binomial coefficient.
== Proof ==
From Lower and Upper Bound of Factorial, we have that:
:$k! \le \dfrac {k^{k + 1} } {e^{k - 1} }$
so that:
:$(1): \quad \dfrac 1 {k!} \ge \dfrac {e^{k - 1} } {k^{k + 1} }$
Then:
Hence the result.
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Exercise $67$
Category:Binomial Coefficients
Lower Bound for Ordinal Exponentiation

== Theorem ==
Let $x$ and $y$ be ordinals.
Let $x$ be greater than $1$, where $1$ denotes the successor of the zero ordinal.
Then:
:$y \le x^y$
== Proof ==
The proof shall proceed by Transfinite Induction on $y$.
=== Basis for the Induction ===
If $y = 0$, then $0 \le x^y$ by Empty Set is Subset of All Sets.
This proves the basis for the induction.
=== Induction Step ===
The induction hypothesis states that:
:$y \le x^y$
This proves the induction step.
=== Limit Case ===
The induction hypothesis for the limit case states that:
:$\forall z \in y: z \le x^z$ and $y$ is a limit ordinal
This proves the limit case.
== Sources ==
* : $\S 8.37$
Category:Ordinal Arithmetic
Lower Bound for Subset

== Theorem ==
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $L$ be a lower bound for $S$.
Let $\left({T, \preceq}\right)$ be a subset of $\left({S, \preceq}\right)$.
Then $L$ is a lower bound for $T$.
== Proof ==
By definition of lower bound:
:$\forall x \in S: L \preceq x$
But as $\forall y \in T: y \in S$ by definition of subset, it follows that:
:$\forall y \in T: L \preceq y$.
Hence the result, again by definition of lower bound.
== Also see ==
* Upper Bound for Subset
Category:Order Theory
Lower Bound is Lower Bound for Subset

== Theorem ==
Let $\struct {S, \preceq}$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
:$B \subseteq A$
Let $L$ be an element of $S$.
Let $L$ be a lower bound for $A$.
Then $L$ is a lower bound for $B$.
== Proof ==
Let $L$ be a lower bound for $A$.
By definition of lower bound:
:$\forall x \in A: L \preceq x$
By definition of subset:
:$\forall x \in B: x \in A$
Hence:
:$\forall x \in B: L \preceq x$
Thus by definition:
:$L$ is a lower bound for $B$.
== Sources ==
* 
Category:Preorder Theory
Lower Bound is Upper Bound for Inverse Ordering

== Definition ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $m$ be a lower bound for $\struct {T, \preceq}$.
Let $\succeq$ be the dual ordering of $\preceq$.
Then $m$ is an upper bound for $\struct {T, \succeq}$.
== Proof ==
Let $m$ be a lower bound for $\struct {T, \preceq}$.
That is:
:$\forall a \in T: m \preceq a$
By definition of dual ordering, it follows that:
:$\forall a \in T: a \succeq m$
That is, $M$ is an upper bound for $\struct {T, \succeq}$.
== Also see ==
* Upper Bound is Lower Bound for Inverse Ordering
Category:Order Theory
Lower Bound of Natural Logarithm

== Theorem ==
:$\forall x \in \R_{>0}: 1 - \dfrac 1 x \le \ln x$
where $\ln x$ denotes the natural logarithm of $x$.
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Illustration ==
== Also see ==
* Bounds of Natural Logarithm
Category:Real Analysis
Category:Logarithms
Category:Inequalities
Category:Lower Bound of Natural Logarithm
Lower Bound of Natural Logarithm/Proof 2

== Theorem ==
== Proof ==
Let $x > 0$.
Note that:
:$1 - \dfrac 1 x \le \ln x$
is logically equivalent to:
:$1 - \dfrac 1 x - \ln x \le 0$
Let $\map f x = 1 - \dfrac 1 x - \ln x$.
Then:
 
Note that $\map {f'} 1 = 0$.
Also, $\map {f} 1 < 0$.
So by the Second Derivative Test, $x = 1$ is a local maximum.
On $\openint 0 1$:
:$\map {f'} x > 0$
By Derivative of Monotone Function, $f$ is strictly increasing on that interval.
On $\openint 1 \to$:
:$\map {f'} x < 0$
By Derivative of Monotone Function, $f$ is strictly decreasing on that interval.
So $x = 1$ yields a global maximum, at which by Logarithm of 1 is 0:
:$\map f 1 = 1 - 1 - 0 = 0$
That is:
:$\forall x > 0: \map f x \le 0$
and so by definition of $\map f x$:
:$1 - \dfrac 1 x - \ln x \le 0$
== Illustration ==
Category:Lower Bound of Natural Logarithm
Lower Bound of Natural Logarithm/Proof 3

== Theorem ==
== Proof ==
Let $\sequence {f_n}$ be the sequence of mappings $f_n: \R_{>0} \to \R$ defined as:
:$\map {f_n} x = n \paren {\sqrt [n] x - 1 }$
Let $x \in \R_{>0}$ be fixed.
We first show that:
:$\forall n \in \N : 1 - \dfrac 1 x \le n \paren {\sqrt [n] x - 1}$
Let $n \in \N$.
From Sum of Geometric Sequence:
:$\sqrt [n] x - 1 = \dfrac {x - 1} {1 + \sqrt [n] x + \sqrt [n] x^2 + \cdots + \sqrt [n] x^{n - 1} }$
=== Case 1: $0 < x < 1$ ===
=== Case 2: $x = 1$ ===
=== Case 3: $x > 1$ ===
Thus:
:$\forall n \in \N : 1 - \dfrac 1 x \le n \paren {\sqrt [n] x - 1 }$
by Proof by Cases.
Thus:
:$\ds 1 - \dfrac 1 x \le \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1 }$
from Limit of Bounded Convergent Sequence is Bounded.
Hence the result, from the definition of $\ln$.
== Illustration ==
Category:Lower Bound of Natural Logarithm
Lower Bound of Pell Number

== Theorem ==
For all $n \in \N$:
:$P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
where:
:$P_n$ is the $n$th Pell number
== Proof ==
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:$P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
=== Basis for the Induction ===
$\map P 1$ is true, as this just says:
:$P_1 = 1 = 2 \paren 2^{-1} \ge 2 \paren {1 + \sqrt 2}^{-1}$
It is also necessary to demonstrate $\map P 2$ is true:
:$P_2 = 2 \ge 2 \paren {1 + \sqrt 2}^0$
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P j$ is true for all $1 \le j \le k$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$P_j \ge 2 \paren {1 + \sqrt 2}^{j - 2}$ for $1 \le j \le k$
from which it is to be shown that:
:$P_{k + 1} \ge 2 \paren {1 + \sqrt 2}^{k - 1}$
=== Induction Step ===
This is the induction step:
As we have already shown $\map P 1$ and $\map P 2$, we just need to prove the result for $k \ge 2$.
So $\map P 1 \land \map P 2 \land \dots \land \map P k \implies \map P {k + 1}$ and the result follows by the Second Principle of Mathematical Induction.
Therefore:
:$\forall n \in \N: P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
Category:Pell Numbers
Lower Bounds for Denominators of Simple Continued Fraction

== Theorem ==
Let $n \in \N \cup \{\infty\}$ be an extended natural number.
Let $\left[{a_0, a_1, a_2, \ldots}\right]$ be a simple continued fraction in $\R$ of length $N$.
Let $q_0, q_1, q_2, \ldots$ be its denominators.
=== Denominator is larger than index ===
For all $k > 4 : q_k > k$.
=== Denominator is at least Fibonacci number ===
Let $F_k$ denote the $k$th Fibonacci number.
For all $k \geq 0$, $q_k \geq F_{k+1}$.
== Proof ==
By Denominators of Simple Continued Fraction are Strictly Increasing, with the possible exception of $1 = q_0 = q_1$, the sequence $\left \langle {q_n}\right \rangle$ is strictly increasing.
Now, since $q_2 > q_1 \ge q_0 = 1$, we have $q_2 \geq 2$.
Then $q_{k+1} \ge q_k + q_{k-1}$ shows that from $q_3$ onwards, the $q_k$s increase in steps of at least $2$.
As $q_3 \ge 3$, it follows that $q_4 \ge 5$.
The result follows.
Category:Simple Continued Fractions
Lower Closure is Closure Operator

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Then
:lower closure of set is a closure operator.
== Proof ==
=== Inflationary ===
Let $X$ be a subset of $S$.
Let $x \in X$.
By definition of reflexivity:
:$x \preceq x$
Thus by definition of lower closure of set:
:$x \in X^\preceq$
Thus by definition of subset:
:$X \subseteq X^\preceq$
=== Increasing ===
Let $X, Y$ be subsets of $S$ such that
:$X \subseteq Y$
Let $x \in X^\preceq$.
By definition of lower closure of set:
:$\exists y \in X: x \preceq y$
By definition of subset:
:$y \in Y$
Thus by definition of lower closure of set:
:$x \in Y^\preceq$
Thus by definition of subset:
:$X^\preceq \subseteq Y^\preceq$
=== Idempotent ===
Let $X$ be a subset of $S$.
Let $x \in \paren {X^\preceq}^\preceq$.
By definition of lower closure of set:
:$\exists y \in X^\preceq: x \preceq y$
By definition of lower closure of set:
:$\exists z \in X: y \preceq z$
By definition of transitivity:
:$x \preceq z$
Thus by definition of lower closure of set:
:$x \in X^\preceq$
Thus by definition of subset:
:$\paren {X^\preceq}^\preceq \subseteq X^\preceq$
By definition of inflationary:
:$X \subseteq X^\preceq$
By definition of increasing:
:$X^\preceq \subseteq \paren {X^\preceq}^\preceq$
Thus definition of set equality;
:$\paren {X^\preceq}^\preceq = X^\preceq$
Thus by definition:
:lower closure of set is a closure operator.
Category:Lower Closures
Category:Closure Operators
Lower Closure is Dual to Upper Closure

== Theorem ==
Let $\left({S, \preccurlyeq}\right)$ be an ordered set.
Let $a, b \in S$.
Let $T \subseteq S$
The following are pairs of dual statements:
:$b \in a^\preccurlyeq$, the lower closure of $a$
:$b \in a^\succcurlyeq$, the upper closure of $a$
:$b \in T^\preccurlyeq$, the lower closure of $T$
:$b \in T^\succcurlyeq$, the upper closure of $T$
== Proof ==
=== Elements ===
By definition of lower closure, $b \in a^\preccurlyeq$ :
:$b \preccurlyeq a$
The dual of this statement is:
:$a \preccurlyeq b$
by Dual Pairs (Order Theory).
By definition of upper closure, this means $b \in a^\succcurlyeq$.
The converse follows from Dual of Dual Statement (Order Theory).
=== Sets ===
By the definition of lower closure, $b \in T^\preccurlyeq$ :
:$\exists a \in T: b \preccurlyeq a$
The dual of this statement is:
:$\exists a \in T: a \preccurlyeq b$
by Dual Pairs (Order Theory).
By the definition of upper closure, this means $b \in T^\succcurlyeq$.
== Also see ==
* Duality Principle (Order Theory)
Category:Upper Closures
Category:Lower Closures
Category:Dual Pairs (Order Theory)
Lower Closure is Increasing

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y$ be elements of $S$ such that
:$x \preceq y$
Then:
:$x^\preceq \subseteq y^\preceq$
where $y^\preceq$ denotes the lower closure of $y$.
== Proof ==
Let $z \in x^\preceq$.
By definition of lower closure of element:
:$z \preceq x$
By definition of transitivity:
:$z \preceq y$
Thus again by definition of lower closure of element:
:$z \in y^\preceq$
== Sources ==
* 
* 
Category:Lower Closures
Lower Closure is Lower Section

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $T$ be a subset of $S$.
Let $L$ be the lower closure of $T$.
Then $L$ is a lower section.
== Proof ==
Let $a \in L$.
Let $b \in S$ with $b \preceq a$.
By the definition of lower closure, there is a $t \in T$ such that $a \preceq t$.
By transitivity, $b \preceq t$.
Thus, again by the definition of lower closure, $b \in L$.
Since this holds for all such $a$ and $b$, $L$ is a lower section.
== Also see ==
* Upper Closure is Upper Section
Category:Lower Sections
Category:Lower Closures
Lower Closure is Prime Ideal for Prime Element

== Theorem ==
Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a lattice.
Let $p \in S$ be a prime element.
Then $p^\preceq$ is a prime ideal.
== Proof ==
Let $x, y \in S$ such that
:$x \wedge y \in p^\preceq$
By definition of lower closure of element:
:$x \wedge y \preceq p$
By Characterization of Prime Ideal:
:$x \preceq p$ or $y \preceq p$
Thus by definition of lower closure of element:
:$x \in p^\preceq$ or $y \in p^\preceq$
== Sources ==
* 
* 
Category:Prime Ideals (Order Theory)
Category:Prime Elements
Lower Closure is Strict Lower Closure of Immediate Successor

== Theorem ==
Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
Let $b$ be the immediate successor element of $a$:
Then:
:$a^\preccurlyeq = b^\prec$
where:
:$a^\preccurlyeq$ is the lower closure of $a$
:$b^\prec$ is the strict lower closure of $b$.
== Proof ==
Let:
:$x \in b^\prec$
By the definition of strict upper closure:
:$x \prec b$
By the definition of total ordering:
:$a \prec x$ or $x \preccurlyeq a$
If $a \prec x$ then $a \prec x \prec b$, contradicting the premise.
Thus:
:$x \preccurlyeq a$
and so:
:$x \in a^\preccurlyeq$
By definition of subset:
:$b^\prec \subseteq a^\preccurlyeq$
Let:
:$x \in a^\preccurlyeq$
By the definition of upper closure:
:$x \preccurlyeq a$
Since $a \prec b$, Extended Transitivity shows that $x \prec b$.
Thus:
:$x \in b^\prec$
By definition of subset:
:$a^\preccurlyeq \subseteq b^\prec$
Therefore by definition of set equality:
:$a^\succ = b^\succcurlyeq$
Category:Total Orderings
Category:Lower Closures
Lower Closure of Directed Subset is Ideal

== Theorem ==
Let $\mathscr S = \struct {S, \preceq}$ be an ordered set.
Let $D$ be a directed subset of $S$.
Then
:$D^\preceq$ is an ideal in $\mathscr S$
where $D^\preceq$ denotes the lower closure of $D$.
== Proof ==
By Directed iff Lower Closure Directed:
:$D^\preceq$ is directed.
By Lower Closure is Lower Section:
:$D^\preceq$ is a lower section.
Thus by definition
:$D^\preceq$ is an ideal in $\mathscr S$
== Sources ==
* 
* 
* 
Category:Order Theory
Lower Closure of Element is Closed under Directed Suprema

== Theorem ==
Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $x \in S$.
Then $x^\preceq$ is closed under directed suprema,
where $x^\preceq$ denotes the lower closure of $x$.
== Proof ==
Let $D$ be a directed subset of $S$ such that
:$D \subseteq x^\preceq$
By Lower Closure of Element is Ideal:
:$x^\preceq$ is directed.
By definition of up-complete:
:$D$ and $x^\preceq$ admit suprema.
By Supremum of Subset:
:$\sup D \preceq \map \sup {x^\preceq}$
By Supremum of Lower Closure of Element:
:$\sup D \preceq x$
Thus by definition of lower closure of element:
:$\sup D \in x^\preceq$
== Sources ==
* 
Category:Order Theory
Lower Closure of Element is Ideal

== Theorem ==
Let $\struct {S, \preceq}$ ne an ordered set.
Let $s$ be an element of $S$.
Then $s^\preceq$ is ideal in $\struct {S, \preceq}$
where $s^\preceq$ denotes the lower closure of $s$.
== Proof ==
By Singleton is Directed and Filtered Subset:
:$\set s$ is a directed subset of $S$
By Directed iff Lower Closure Directed:
:$\set s^\preceq$ is a directed subset of $S$
By Lower Closure is Lower Section:
:$\set s^\preceq$ is a lower section in $S$
By Lower Closure of Singleton
:$\set s^\preceq = s^\preceq$
By definition of reflexivity:
:$s \preceq s$
By definition of lower closure of element:
:$s \in s^\preceq$
Thus by definition:
:$s^\succeq$ is non-empty, directed and lower.
Thus by definition:
:$s^\preceq$ is a ideal in $\struct {S, \preceq}$
== Sources ==
* 
* 
* 
Category:Lower Closures
Lower Closure of Element is Topologically Closed in Scott Topological Ordered Set

== Theorem ==
Let $\struct {S, \preceq}$ be an up-complete ordered set.
Let $T = \struct {S, \preceq, \tau}$ be a relational structure with the Scott topology.
Let $x \in S$.
Let $x^\preceq$ denote the lower closure of $x$.
Then $x^\preceq$ is topologically closed.
== Proof ==
By Lower Closure of Element is Closed under Directed Suprema:
:$x^\preceq$ is closed under directed suprema.
By Lower Closure of Singleton:
:$\set x^\preceq = x^\preceq$
By Lower Closure is Lower Section:
:$x^\preceq$ is a lower section.
Thus by Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set:
:$x^\preceq$ is closed.
== Sources ==
* 
* 
Category:Topological Order Theory
Category:Closed Sets