nyuuzyou/wikis huggingface dataset:
Way Below Relation is Antisymmetric

== Theorem ==
Let $\struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x \ll y$ and $y \ll x$
Then
:$x = y$
== Proof ==
By Way Below implies Preceding:
:$x \preceq y$ and $y \preceq x$
Thus by definition of antisymmetry:
:$x = y$
== Sources ==
* 
* 
Category:Way Below Relation
Way Below Relation is Auxiliary Relation

== Theorem ==
Lrt $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.
Then
:$\ll$ is auxiliary relation
where $\ll$ denotes the way below relation.
== Proof ==
By Way Below implies Preceding:
:$\forall x, y \in S: x \ll y \implies x \preceq y$
By Preceding and Way Below implies Way Below:
:$\forall x, y, z, u \in S: x \preceq y \ll z \preceq u \implies x \ll u$
By Join is Way Below if Operands are Way Below:
:$\forall x, y, z \in S: x \ll z \land y \ll z \implies x \vee y \ll z$
By Bottom is Way Below Any Element:
:$\forall x: \bot \ll x$
where $\bot$ denotes the smallest element in $L$.
Thus by definition:
:$\ll$ is auxiliary relation.
== Sources ==
* 
* 
Category:Auxiliary Relations
Category:Way Below Relation
Way Below Relation is Multiplicative implies Pseudoprime Element is Prime

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice such that
:$\ll$ is multiplicative relation
where $\ll$ denotes the way below relation of $L$.
Let $p \in S$.
Then $p$ is a pseudoprime element is a prime element.
== Proof ==
Let $p$ be a pseudoprime element.
:
:$p$ is not a prime element.
By definition of prime element:
:$\exists x, y \in S: x \wedge y \preceq p$ and $x \npreceq p$ and $y \npreceq p$
By definition of continuous:
:$\forall z \in S: z^\ll$ is directed.
and
:$L$ satisfies the axiom of approximation.
By Axiom of Approximation in Up-Complete Semilattice:
:$\exists u \in S: u \ll x \land u \npreceq p$
and
:$\exists v \in S: v \ll y \land v \npreceq p$
By Way Below Relation is Auxiliary Relation:
:$\ll$ is auxiliary relation.
By Multiplicative Auxiliary Relation iff Congruent:
:$u \wedge v \ll x \wedge y$
By definition of transitivity:
:$u \wedge v \ll p$
By Characterization of Pseudoprime Element when Way Below Relation is Multiplicative:
:$u \preceq p$ or $v \preceq p$
This contradicts $u \npreceq p$ and $v \npreceq p$
== Sources ==
* 
* 
Category:Prime Elements
Category:Way Below Relation
Way Below Relation is Transitive

== Theorem ==
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $x, y, z \in S$ such that
:$x \ll y \ll z$
Then
:$x \ll z$
== Proof ==
By Way Below implies Preceding:
:$x \preceq y$
By definition of reflexivity:
:$z \preceq z$
Thus by Preceding and Way Below implies Way Below:
:$x \ll z$
== Sources ==
* 
* 
Category:Way Below Relation
Way Below has Interpolation Property

== Theorem ==
Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.
Let $x, z \in S$ such that
:$x \ll z$
Then
:$\exists y \in S: x \ll y \land y \ll z$
== Proof ==
Case $x \ne z$:
By Way Below has Strong Interpolation Property:
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$
Thus
:$\exists y \in S: x \ll y \land y \ll z$
Case $x = z$:
Define $y = x$
Thus
:$x \ll y \land y \ll z$
== Sources ==
* 
* 
Category:Continuous Lattices
Category:Way Below Relation
Way Below has Strong Interpolation Property

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Let $x, z \in S$ such that
:$x \ll z \land x \ne z$
Then
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$
== Proof ==
By Way Below is Approximating Relation and Way Below Relation is Auxiliary Relation:
:$\ll$ is an auxiliary approximating relation on $S$.
Thus by Auxiliary Approximating Relation has Interpolation Property:
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$
== Sources ==
* 
* 
Category:Approximating Relations
Category:Continuous Lattices
Category:Way Below Relation
Way Below if Between is Compact Set in Ordered Set of Topology

== Theorem ==
Let $T = \struct {S, \tau}$ be a topological space.
Let $L = \struct {\tau, \preceq}$ be an ordered set
where $\preceq \mathop = \subseteq\restriction_{\tau \times \tau}$
Let $x, y \in \tau$ such that:
:$\exists H \subseteq S: x \subseteq H \subseteq y \land H$ is compact
Then:
:$x \ll y$
== Proof ==
Let $D$ be a directed subset of $\tau$ such that:
:$y \preceq \sup D$
By proof of Topology forms Complete Lattice:
:$\ds y \subseteq \bigcup D$
By Subset Relation is Transitive:
:$\ds H \subseteq \bigcup D$
By definition:
:$D$ is open cover of $H$
By definition of compact:
:$H$ has finite subcover $\GG$ of $D$
By Directed iff Finite Subsets have Upper Bounds:
:$\exists d \in D: d$ is upper bound for $\GG$
By definitions of upper bound and of $\preceq$:
:$\forall z \in \GG: z \subseteq d$
By Union is Smallest Superset/Set of Sets:
:$\ds \bigcup \GG \subseteq d$
By definition of cover:
:$\ds H \subseteq \bigcup \GG$
By Subset Relation is Transitive:
:$x \subseteq d$
Thus by definition of $\preceq$:
:$x \preceq d$
Thus by definition of way below relation:
:$x \ll y$
== Sources ==
* 
* 
Category:Way Below Relation
Category:Topology
Way Below iff Preceding Finite Supremum

== Theorem ==
Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$.
Then $x \ll y$ 
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it Fin} X: x \preceq \sup A$
where
:$\ll$ denotes the way below relation,
:$\map {\it Fin} X$ denotes the set of all finite subsets of $X$.
== Proof ==
=== Sufficient Condition ===
Let $x \ll y$
Let $X \subseteq S$ such that:
:$y \preceq \sup X$
Define:
:$F := \set {\sup A: A \in \map {\it Fin} X}$
By definition of union:
:$X = \bigcup \map {\it Fin} X$
By Supremum of Suprema:
:$\sup X = \sup F$
We will prove that:
:$F$ is directed
Let $a, b \in F$.
By definition of $F$:
:$\exists A \in \map {\it Fin} X: a = \sup A$
and
:$\exists B \in \map {\it Fin} X: b = \sup B$
By Union of Subsets is Subset:
:$A \cup B \subseteq X$
By Finite Union of Finite Sets is Finite:
:$A \cup B$ is finite
By definition of ${\it Fin}$:
:$A \cup B \in \map {\it Fin} X$
By definition of $F$:
:$\map \sup {A \cup B} \in F$
By Set is Subset of Union:
:$A \subseteq A \cup B$ and $B \subseteq A \cup B$
By Supremum of Subset:
:$a \preceq \map \sup {A \cup B}$ and $b \preceq \map \sup {A \cup B}$
Thus by definition:
:$F$ is directed
By definition of way below relation:
:$\exists d \in F: x \preceq d$
Thus by definition of $F$:
:$\exists A \in \map {\it Fin} X: x \preceq \sup A$
=== Necessary Condition ===
Assume that:
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\it Fin} X: x \preceq \sup A$
Let $D$ be a directed subset of $S$ such that:
:$y \preceq \sup D$
By assumption:
:$\exists A \in \map {\it Fin} D: x \preceq \sup A$
By Directed iff Finite Subsets have Upper Bounds:
:$\exists h \in D: \forall a \in A: a \preceq h$
By definition:
:$h$ is upper bound for $A$
By definition of supremum:
:$\sup A \preceq h$
Thus by definition of transitivity:
:$x \preceq h$
Thus by definition of way below relation:
:$x \ll y$
== Sources ==
* 
* 
* 
Category:Way Below Relation
Way Below iff Second Operand Preceding Supremum of Directed Set There Exists Element of Directed Set First Operand Way Below Element

== Theorem ==
Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.
Let $x, y$ be elements of $S$.
Then
:$x \ll y$
:for every directed subset $D$ of $S$ such that $y \preceq \sup D$
::there exists an element $d$ of $D$: $x \ll d$
== Proof ==
=== Sufficient Condition ===
Let $x \ll y$.
Let $D$ be a directed subset of $S$ such that
:$y \preceq \sup D$
By Way Below has Interpolation Property:
:$\exists x' \in S: x \ll x' \land x' \ll y$
By definition of way below relation:
:$\exists d \in D: x' \preceq d$
Thus by Preceding and Way Below implies Way Below and definition of reflexivity:
:$x \ll d$
=== Necessary Condition ===
Assume that
:for every directed subset $D$ of $S$ such that $y \preceq \sup D$
::there exists an element $d$ of $D$: $x \ll d$
By Way Below implies Preceding:
:for every directed subset $D$ of $S$ such that $y \preceq \sup D$
::there exists an element $d$ of $D$: $x \preceq d$
Thus by definition of way below relation:
$x \ll y$
== Sources ==
* 
* 
Category:Way Below Relation
Category:Continuous Lattices
Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal

== Theorem ==
Let $\mathscr S = \struct {S, \preceq}$ be an up-complete ordered set.
Let $x, y \in S$.
Then $x \ll y$ 
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.
== Proof ==
=== Sufficient Condition ===
Let $x \ll y$
Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that
:$y \preceq \sup I$
By definition of ideal:
:$I$ is directed and lower.
By definition of up-complete:
:$I$ admits a supremum.
By definition of way below relation:
:$\exists i \in I: x \preceq i$
Thus by definition of lower section:
:$x \in I$
=== Necessary Condition ===
Assume that
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$
Let $D$ be a directed subset of $S$ such that:
:$D$ admits a supremum and $y \preceq \sup D$
By Supremum of Lower Closure of Set:
:$D^\preceq$ admits a supremum and $\sup D^\preceq = \sup D$
where $D^\preceq$ denotes the lower closure of $D$.
By Lower Closure of Directed Subset is Ideal:
:$D^\preceq$ is an ideal.
By assumption:
:$x \in D^\preceq$
Thus by definition of lower closure of subset:
:$\exists d \in D: x \preceq d$
Thus by definition of way below relation:
:$x \ll y$
== Sources ==
* 
* 
* 
Category:Way Below Relation
Way Below iff Second Operand Preceding Supremum of Prime Ideal implies First Operand is Element of Ideal

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive complete lattice.
Let $x, y \in S$.
Then $x \ll y$ :
:for every prime ideal $P$ in $L$: $y \preceq \sup P \implies x \in P$
== Proof ==
=== Sufficient Condition ===
The result follows by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal.
=== Necessary Condition ===
Suppose
:for every prime ideal $P$ in $L$:
:$y \preceq \sup P \implies x \in P$
We will prove that:
:for every ideal $I$ in $L$: $y \preceq \sup I \implies x \in I$
Let $I$ be an ideal in $L$ such that
:$y \preceq \sup I$
:$x \notin I$
By If Element Does Not Belong to Ideal then There Exists Prime Ideal Including Ideal and Excluding Element:
:there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $x \notin P$
By Supremum of Subset:
:$\sup I \preceq \sup P$
By definition of transitivity:
:$y \preceq \sup P$
By assumption:
:$x \in P$
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \ll y$
== Sources ==
* 
* 
Category:Prime Ideals (Order Theory)
Category:Way Below Relation
Way Below implies Preceding

== Theorem ==
Let $\left({S, \preceq}\right)$ be an ordered set.
Let $x, y \in S$ such that
:$x \ll y$
where $\ll$ denotes element is way below second element.
Then
:$x \preceq y$
== Proof ==
By Singleton is Directed and Filtered Subset:
:$\left\{ {y}\right\}$ is directed.
By Supremum of Singleton:
:$\left\{ {y}\right\}$ admits a supremum and $\sup \left\{ {y}\right\} = y$
By definition of reflexivity:
:$y \preceq \sup \left\{ {y}\right\}$
By definition of way below:
:$\exists d \in \left\{ {y}\right\}: x \preceq d$
Thus by definition of singleton:
:$x \preceq y$
== Sources ==
* 
* 
Category:Way Below Relation
Way Below in Complete Lattice

== Theorem ==
Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$.
Then
:$x \ll y$
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.
== Proof ==
=== Sufficient Condition ===
Let
:$x \ll y$
Let $X \subseteq S$ such that
:$y \preceq \sup X$
By Set of Finite Suprema is Directed:
:$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
By definition of union:
:$\bigcup \map {\operatorname {Fin} } X \setminus \set \O = X$
By Supremum of Suprema:
:$\sup X = \sup \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
By definition of way below relation:
:$\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}: x \preceq z$
Thus
:$\exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
=== Necessary Condition ===
Let
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
Let $D$ be a directed subset of $S$ such that
:$y \preceq \sup D$
By assumption:
:$\exists A \in \map {\operatorname {Fin} } D: x \preceq \sup A$
By Directed iff Finite Subsets have Upper Bounds:
:$\exists u \in D: u$ is upper bound for $A$
By definition of supremum:
:$\sup A \preceq u$
Thus by definition of transitivity:
:$x \preceq u$
Thus by definition of way below relation:
:$x \ll y$
== Sources ==
* 
* 
* 
Category:Way Below Relation
Category:Complete Lattices
Way Below in Lattice of Power Set

== Theorem ==
Let $X$ be a set.
Let $L = \struct {\powerset X, \cup, \cap, \preceq}$ be a lattice of power set of $X$ where $\mathord\preceq = \mathord\subseteq \cap \paren {\powerset X \times \powerset X}$
Let $x, y \in \powerset X$.
Then $x \ll y$ 
:for every a set $Y$ of subsets of $X$ such that $y \subseteq \bigcup Y$
::then there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
where $\ll$ denotes the way below relation.
== Proof ==
=== Sufficient Condition ===
Let $x \ll y$
Let $Y$ be a set of subsets of $X$ such that
:$y \subseteq \bigcup Y$
By definitions of power set and subset:
:$Y \subseteq \powerset X$
By Power Set is Complete Lattice:
:$\bigcup Y = \sup Y$
By definition of $\preceq$:
:$y \preceq \sup Y$
By Way Below in Complete Lattice:
:there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
By the proof of Power Set is Complete Lattice:
:$\bigcup Z = \sup Z$
Thus by definition of $\preceq$:
:there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
=== Necessary Condition ===
Suppose
:for every a set $Y$ of subsets of $X$ such that $y \subseteq \bigcup Y$
::then there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
We will prove that
:for every a subset $Y$ of $\powerset X$ such that $y \preceq \sup Y$
::then there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
Let $Y$ be a subset of $\powerset X$ such that
:$y \preceq \sup Y$
By definition of power set:
:$Y$ is a set of subsets of $X$.
By Power Set is Complete Lattice:
:$\bigcup Y = \sup Y$
By definition of $\preceq$:
:$y \subseteq \bigcup Y$
By assumption:
:there exists a finite subset $Z$ of $Y$: $x \subseteq \bigcup Z$
By the proof of Power Set is Complete Lattice:
:$\bigcup Z = \sup Z$
Thus by definition of $\preceq$:
:there exists a finite subset $Z$ of $Y$: $x \preceq \sup Z$
Thus by Way Below in Complete Lattice:
:$x \ll y$
== Sources ==
* 
* 
Category:Way Below Relation
Category:Power Set
Way Below in Meet-Continuous Lattice

== Theorem ==
Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be a meet-continuous bounded below lattice.
Let $x, y \in S$.
Then $x \ll y$ 
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y = \sup I \implies x \in I$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.
== Proof ==
=== Sufficient Condition ===
Let $x \ll y$
Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that
:$y = \sup I$
By definition of reflexivity:
:$y \preceq \sup I$
By definition of meet-continuous:
:$\mathscr S$ is up-complete.
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \in I$
=== Necessary Condition ===
Assume:
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y = \sup I \implies x \in I$
We will prove that:
:$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$
Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that
:$y \preceq \sup I$
By definition of ideal:
:$I$ is directed and lower.
Define $Y := \set {y \wedge d: d \in I}$
By Set of Finite Suprema is Directed:
:$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}$ is directed.
where $\map {\operatorname {Fin} } Y$ denotes the set of all finite subsets of $Y$.
By definition of up-complete:
:$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}$ admits a supremum.
By definition of union:
:$Y = \bigcup \map {\operatorname {Fin} } Y$
where $^\preceq$ denotes the lower closure of set.
By Lower Closure of Directed Subset is Ideal:
:$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}^\preceq$ is an ideal in $\mathscr S$
By assumption:
:$x \in \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}^\preceq$
By definition of lower closure of set:
:$\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}: x \preceq z$
Then
:$\exists A \in \map {\operatorname {Fin} } Y: z = \sup A \land A \ne \O$
We will prove as a sublemma that:
:$A \subseteq I$
Let $a \in A$.
By definition of subset:
:$a \in Y$
By definition of $Y$:
:$\exists i \in I: a = y \wedge i$
By Meet Precedes Operands:
:$a \preceq i$
Thus by definition of lower section:
:$a \in I$
This ends the proof of sublemma.
By Directed iff Finite Subsets have Upper Bounds:
:$\exists h \in I: \forall a \in A: a \preceq h$
By definition:
:$h$ is upper bound for $A$
By definition of supremum:
:$z = \sup A \preceq h$
By definition of transitivity:
:$x \preceq h$
Thus by definition of lower section:
:$x \in I$
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \ll y$
== Sources ==
* 
* 
Category:Way Below Relation
Category:Meet-Continuous Lattices
Way Below in Ordered Set of Topology

== Theorem ==
Let $\struct {S, \tau}$ be a topological space.
Let $\struct {\tau, \preceq}$ be an ordered set
where $\preceq \mathop = \subseteq \restriction_{\tau \times \tau}$
Let $x, y \in \tau$.
Then:
:$x \ll y$ in $\struct {\tau, \preceq}$
:for every set $F$ of open subsets of $S$: if $y \subseteq \bigcup F$, then:
::there exists a finite subset $G$ of $F$: $x \subseteq \bigcup G$
where $\ll$ denotes the way below relation.
== Proof ==
=== Sufficient Condition ===
Let
:$x \ll y$
Let $F$ be a set of open subsets of $S$ such that
:$y \subseteq \bigcup F$
By definition of subset:
:$F \subseteq \tau$
By proof of Topology forms Complete Lattice:
:$\sup F = \bigcup F$
By assumption:
:$y \preceq \sup F$
By Topology forms Complete Lattice:
:$\struct {\tau, \preceq}$ is complete lattice.
By Way Below in Complete Lattice:
:$\exists G \in \map {\it Fin} F: x \preceq \sup G$
where $\map {\it Fin} F$ denotes the set of all finite subsets of $F$.
Thus by proof of Topology forms Complete Lattice:
:$x \subseteq \bigcup G$
=== Necessary Condition ===
Assume that
:for every set $F$ of open subsets of $S$: if $y \subseteq \bigcup F$, then
::there exists a finite subset $G$ of $F$: $x \subseteq \bigcup G$
Let $I$ be an ideal in $\struct {\tau, \preceq}$ such that
:$y \preceq \sup I$
By proof of Topology forms Complete Lattice:
:$y \subseteq \bigcup I$
By assumption:
:there exists a finite subset $G$ of $I$: $x \subseteq \bigcup G$
By proof of Topology forms Complete Lattice:
:$x \preceq \sup I$
By definition of ideal:
:$I$ is directed and lower.
By Directed iff Finite Subsets have Upper Bounds:
:$\exists u \in I: u$ is upper bound for $G$
By definition of supremum:
:$\sup G \preceq u$
By definition of transitivity:
:$x \preceq u$
Thus by definition of lower section:
:$x \in I$
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$x \ll y$
== Sources ==
* 
* 
* 
Category:Way Below Relation
Category:Topology
Way Below is Approximating Relation

== Theorem ==
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Then $\ll$ is an approximating relation on $S$.
== Proof ==
Let $x \in S$.
Define $\RR := \mathord \ll$.
By definitions of way below closure and $\RR$-segment:
:$x^\ll = x^\RR$
where:
:$x^\ll$ denotes the way below closure of $x$
:$x^\RR$ denotes the $\RR$-segment of $x$
By definition of continuous:
:$L$ satisfies the axiom of approximation.
Thus by the axiom of approximation:
:$x = \map \sup {x^\ll} = \map \sup {x^\RR}$
Hence $\ll$ is an approximating relation on $S$.
== Sources ==
* 
* 
Category:Approximating Relations
Category:Continuous Lattices
Category:Way Below Relation
Way Below is Congruent for Join

== Theorem ==
Let $L = \left({S, \vee, \preceq}\right)$ be a join semilattice.
Then $\ll$ is congruence relation for $\vee$:
:$\forall a, b, x, y \in S: a \ll x \land b \ll y \implies a \vee b \ll x \vee y$
where $\ll$ denotes the way below relation.
== Proof ==
Let $a, b, x, y \in S$ such that
$a \ll x$ and $b \ll y$
By Join Succeeds Operands:
:$x \preceq x \vee y$ and $y \preceq x \vee y$
By Preceding and Way Below implies Way Below and definition of reflexivity:
:$a \ll x \vee y$ and $b \ll x \vee y$
Thus by Join is Way Below if Operands are Way Below:
:$a \vee b \ll x \vee y$
== Sources ==
* 
* 
Category:Way Below Relation
Weak-* Closed Linear Subspace of Normed Dual Space is Isometrically Isomorphic to a Normed Dual Space

== Theorem ==
Let $X$ be a Banach space. 
Let $X^\ast$ be the normed dual space of $X$. 
Let $w^\ast$ be the weak-$\ast$ topology on $X^\ast$.
Let $Y$ be a linear subspace of $X^\ast$ closed in $\struct {X^\ast, w^\ast}$.
Then there exists a normed vector space $Z$ such that:
:$Y$ is isometrically isomorphic to $Z^\ast$. 
== Proof ==
From Set is Closed iff Equals Topological Closure, we have:
:$\map {\cl_{w^\ast} } Y = Y$
From Closure in Weak-* Topology in terms of Annihilators, we have:
:$Y = \paren { {}^\bot Y}^\bot$
where:
:${}^\bot Y$ denotes the annihilator of $Y \subseteq X^\ast$
:$\paren { {}^\bot Y}^\bot$ denotes the annihilator of ${}^\bot Y \subseteq X$.
From Normed Dual Space of Normed Quotient Vector Space is Isometrically Isomorphic to Annihilator, we have that: 
:$Y = \paren { {}^\bot Y}^\bot$ is isometrically isomorphic to $\paren {X/{}^\bot Y}^\ast$.
Setting $W = {}^\bot Y$ and:
:$Z = X/W$
we get the result.
Category:Weak-* Topologies
Category:Normed Dual Spaces
Weak-* Dense Subset of Normed Dual Space Separates Points

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $X$ be a normed vector space over $\GF$. 
Let $X^\ast$ be the normed dual space of $X$. 
Let $w^\ast$ be the weak-$\ast$ topology on $X^\ast$.
Let $D$ be everywhere dense in $\struct {X^\ast, w^\ast}$. 
Then $D$ separates points.
== Proof ==
Suppose that $D$ is everywhere dense in $\struct {X^\ast, w^\ast}$.
Let $x, y \in X$ be such that: 
:$\map f x = \map g x$ for each $f, g \in D$.
Then: 
:$\map {x^\wedge} f = \map {x^\wedge} g$ for each $f, g \in D$. 
From Characterization of Continuity of Linear Functional in Weak-* Topology, $x^\wedge : \struct {X^\ast, w^\ast} \to \GF$ is continuous. 
From Metric Space is Hausdorff, $\GF$ is Hausdorff.
By hypothesis, $D$ is everywhere dense in $\struct {X^\ast, w^\ast}$.
Hence from Continuous Mappings into Hausdorff Space coinciding on Everywhere Dense Set coincide, we obtain: 
:$\map {x^\wedge} f = \map {x^\wedge} g$ for each $f, g \in X^\ast$.
Then: 
:$\map f x = \map g x$ for each $f, g \in X^\ast$.
From Normed Dual Space Separates Points, we obtain $x = y$.
Category:Weak-* Topologies