theory Topology_ZF_examples_1 imports Topology_ZF_1 Order_ZF
begin
In this theory file we reformulate the concepts related to a topology in relation with a base of the topology and we give examples of topologies defined by bases or subbases.
The topology of a base
Given a family of subsets satisfying the base condition, it is possible to construct a topology where that family is a base of. Even more, it is the only topology with such characteristics.
We define the topology generated by a base satisfying the base condition as the unique topology for which that family is a base.
definition
\( U \text{ satisfies the base condition } \Longrightarrow TopologyBase U \equiv \text{The } T.\ U \text{ is a base for } T \)
If a collection \(U\) of sets satisfies the base condition then the topology constructed from it is indeed a topology and \(U\) is a base for this topology.
theorem Base_topology_is_a_topology:
assumes \( U \text{ satisfies the base condition } \)
shows \( (TopologyBase U) \text{ is a topology } \) and \( U \text{ is a base for } (TopologyBase U) \)proof from assms obtain \( T \) where I: \( U \text{ is a base for } T \) using Top_1_2_T1(2)
then have II: \( \bigwedge S.\ U \text{ is a base for } S \Longrightarrow S=T \) using same_base_same_top
from assms have III: \( TopologyBase U \equiv \text{The } T.\ U \text{ is a base for } T \) using TopologyWithBase_def
from I, II have \( \exists !T.\ U \text{ is a base for } T \) by (rule ex1I )
then have IV: \( U \text{ is a base for } (\text{The } T.\ U \text{ is a base for } T) \) by (rule theI )
with III show \( U \text{ is a base for } (TopologyBase U) \)
with assms show \( (TopologyBase U) \text{ is a topology } \) using Top_1_2_T1(1), IsAbaseFor_def
qed
A base doesn't need the empty set.
lemma base_no_0:
shows \( B\text{ is a base for }T \longleftrightarrow (B-\{0\})\text{ is a base for }T \)proof{
}
fix \( M \)
assume \( M\in \{\bigcup A .\ A \in Pow(B)\} \)
then obtain \( Q \) where \( M=\bigcup Q \), \( Q\in Pow(B) \)
hence \( M=\bigcup (Q-\{0\}) \), \( Q-\{0\}\in Pow(B-\{0\}) \)
hence \( M\in \{\bigcup A .\ A \in Pow(B - \{0\})\} \)
hence \( \{\bigcup A .\ A \in Pow(B)\} \subseteq \{\bigcup A .\ A \in Pow(B - \{0\})\} \)
moreover {
}
qed
fix \( M \)
assume \( M\in \{\bigcup A .\ A \in Pow(B-\{0\})\} \)
then obtain \( Q \) where \( M=\bigcup Q \), \( Q\in Pow(B-\{0\}) \)
hence \( M=\bigcup (Q) \), \( Q\in Pow(B) \)
hence \( M\in \{\bigcup A .\ A \in Pow(B)\} \)
hence \( \{\bigcup A .\ A \in Pow(B - \{0\})\} \subseteq \{\bigcup A .\ A \in Pow(B)\} \)
ultimately have \( \{\bigcup A .\ A \in Pow(B - \{0\})\} = \{\bigcup A .\ A \in Pow(B)\} \)
then show \( B\text{ is a base for }T \longleftrightarrow (B-\{0\})\text{ is a base for }T \) using IsAbaseFor_def
The interior of a set is the union of all the sets of the base which are fully contained by it.
lemma interior_set_base_topology:
assumes \( U \text{ is a base for } T \), \( T\text{ is a topology } \)
shows \( \text{Interior}(A,T) = \bigcup \{T\in U.\ T\subseteq A\} \)proof have \( \{T\in U.\ T\subseteq A\}\subseteq U \)
with assms(1) have \( \bigcup \{T\in U.\ T\subseteq A\}\in T \) using IsAbaseFor_def
moreover
{
have \( \bigcup \{T\in U.\ T\subseteq A\} \subseteq A \)
ultimately show \( \bigcup \{T\in U.\ T\subseteq A\} \subseteq \text{Interior}(A,T) \) using assms(2), Top_2_L5, topology0_def
fix \( x \)
assume \( x \in \text{Interior}(A,T) \)
with assms obtain \( V \) where \( V\in U \), \( V \subseteq \text{Interior}(A,T) \), \( x\in V \) using point_open_base_neigh, Top_2_L2, topology0_def
with assms have \( V\in U \), \( x\in V \), \( V\subseteq A \) using Top_2_L1, topology0_def
hence \( x \in \bigcup \{T\in U.\ T\subseteq A\} \)
thus \( \text{Interior}(A, T) \subseteq \bigcup \{T \in U .\ T \subseteq A\} \)
qed
In the following, we offer another lemma about the closure of a set given a basis for a topology. This lemma is based on cl_inter_neigh and inter_neigh_cl. It states that it is only necessary to check the sets of the base, not all the open sets.
lemma closure_set_base_topology:
assumes \( U \text{ is a base for } Q \), \( Q\text{ is a topology } \), \( A\subseteq \bigcup Q \)
shows \( \text{Closure}(A,Q) = \{x\in \bigcup Q.\ \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0\} \)proof{
}
}
fix \( x \)
assume A: \( x\in \text{Closure}(A,Q) \)
with assms(2,3) have B: \( x\in \bigcup Q \) using topology0_def, Top_3_L11(1)
moreover {
}
fix \( T \)
assume \( T\in U \), \( x\in T \)
with assms(1) have \( T\in Q \), \( x\in T \) using base_sets_open
with assms(2,3), A have \( A\cap T \neq 0 \) using topology0_def, cl_inter_neigh
hence \( \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0 \)
ultimately have \( x\in \{x\in \bigcup Q.\ \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0\} \)
thus \( \text{Closure}(A, Q) \subseteq \{x\in \bigcup Q.\ \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0\} \)
{
fix \( x \)
assume AS: \( x\in \{x \in \bigcup Q .\ \forall T\in U.\ x \in T \longrightarrow A \cap T \neq 0\} \)
hence \( x\in \bigcup Q \)
moreover {
}
}
}
fix \( R \)
assume \( R\in Q \)
with assms(1) obtain \( W \) where RR: \( W\subseteq U \), \( R=\bigcup W \) using IsAbaseFor_def
{
assume \( x\in R \)
with RR(2) obtain \( WW \) where TT: \( WW\in W \), \( x\in WW \)
{
assume \( R\cap A=0 \)
with RR(2), TT(1) have \( WW\cap A=0 \)
with TT(1), RR(1) have \( WW\in U \), \( WW\cap A=0 \)
with AS have \( x\in \bigcup Q-WW \)
with TT(2) have \( False \)
hence \( R\cap A\neq 0 \)
hence \( \forall U\in Q.\ x\in U \longrightarrow U\cap A\neq 0 \)
ultimately have \( x\in \text{Closure}(A,Q) \) using assms(2,3), topology0_def, inter_neigh_cl
then show \( \{x \in \bigcup Q .\ \forall T\in U.\ x \in T \longrightarrow A \cap T \neq 0\} \subseteq \text{Closure}(A,Q) \)
qed
The restriction of a base is a base for the restriction.
lemma subspace_base_topology:
assumes \( B \text{ is a base for } T \)
shows \( (B \text{ restricted to } Y) \text{ is a base for } (T \text{ restricted to } Y) \)proof from assms have \( (B \text{ restricted to } Y) \subseteq (T \text{ restricted to } Y) \) unfolding IsAbaseFor_def, RestrictedTo_def
moreover
qed
have \( (T \text{ restricted to } Y) = \{\bigcup A.\ A \in Pow(B \text{ restricted to } Y)\} \)proof
ultimately show \( thesis \) unfolding IsAbaseFor_def
{
}
}
fix \( U \)
assume \( U \in (T \text{ restricted to } Y) \)
then obtain \( W \) where W: \( W\in T \) and U: \( U = W\cap Y \) unfolding RestrictedTo_def
with assms obtain \( C \) where CB: \( C\in Pow(B) \) and WC: \( W=\bigcup C \) unfolding IsAbaseFor_def
let \( A = \{V\cap Y.\ V\in C\} \)
from CB, U, WC have \( A \in Pow(B \text{ restricted to } Y) \) and UA: \( U=\bigcup A \) unfolding RestrictedTo_def
hence \( U \in \{\bigcup A.\ A \in Pow(B \text{ restricted to } Y)\} \)
thus \( (T \text{ restricted to } Y) \subseteq \{\bigcup A.\ A \in Pow(B \text{ restricted to } Y)\} \)
{
fix \( U \)
assume \( U \in \{\bigcup A.\ A \in Pow(B \text{ restricted to } Y)\} \)
then obtain \( A \) where A: \( A \subseteq (B \text{ restricted to } Y) \) and UA: \( U = (\bigcup A) \)
let \( A_0 = \{C\in B.\ Y\cap C\in A\} \)
from A have \( A_0 \subseteq B \) and \( A = A_0 \text{ restricted to } Y \) unfolding RestrictedTo_def
with UA have \( A_0 \subseteq B \) and \( U = \bigcup (A_0 \text{ restricted to } Y) \)
with assms have \( U \in (T \text{ restricted to } Y) \) unfolding RestrictedTo_def, IsAbaseFor_def
thus \( \{\bigcup A.\ A \in Pow(B \text{ restricted to } Y)\} \subseteq (T \text{ restricted to } Y) \)
qed
If the base of a topology is contained in the base of another topology, then the topologies maintain the same relation.
theorem base_subset:
assumes \( B\text{ is a base for }T \), \( B2\text{ is a base for }T2 \), \( B\subseteq B2 \)
shows \( T\subseteq T2 \)proof{
}
qed
fix \( x \)
assume \( x\in T \)
with assms(1) obtain \( M \) where \( M\subseteq B \), \( x=\bigcup M \) using IsAbaseFor_def
with assms(3) have \( M\subseteq B2 \), \( x=\bigcup M \)
with assms(2) show \( x\in T2 \) using IsAbaseFor_def
Dual Base for Closed Sets
A dual base for closed sets is the collection of complements of sets of a base for the topology.
Given a base \(B\) for a topology \(T\), the dual base consists of the complements \(\bigcup T \setminus U\) for each \(U \in B\), together with the whole space \(\bigcup T\).
definition
\( B\text{ is a base for }T \Longrightarrow DualBase B T\equiv \{\bigcup T-U.\ U\in B\}\cup \{\bigcup T\} \)
Every closed set can be written as an intersection of sets from the dual base.
lemma closed_inter_dual_base:
assumes \( D\text{ is closed in }T \), \( B\text{ is a base for }T \)
obtains \( M \) where \( M\subseteq DualBase B T \), \( D=\bigcap M \)proof assume K: \( \bigwedge M.\ M \subseteq DualBase B T \Longrightarrow D = \bigcap M \Longrightarrow thesis \)
{
assume AS: \( D\neq \bigcup T \)
from assms(1) have D: \( D\in Pow(\bigcup T) \), \( \bigcup T-D\in T \) using IsClosed_def
hence A: \( \bigcup T-(\bigcup T-D)=D \), \( \bigcup T-D\in T \)
with assms(2) obtain \( Q \) where QQ: \( Q\in Pow(B) \), \( \bigcup T-D=\bigcup Q \) using IsAbaseFor_def
{
assume \( Q=0 \)
then have \( \bigcup Q=0 \)
with QQ(2) have \( \bigcup T-D=0 \)
with D(1) have \( D=\bigcup T \)
with AS have \( False \)
hence QNN: \( Q\neq 0 \)
from QQ(2), A(1) have \( D=\bigcup T-\bigcup Q \)
with QNN have \( D=\bigcap \{\bigcup T-R.\ R\in Q\} \)
moreover
from this, assms(2), QQ(1) have \( \{\bigcup T-R.\ R\in Q\}\subseteq DualBase B T \) using DualBase_def
ultimately have \( thesis \) using K
moreover {
}
ultimately show \( thesis \)
qed
assume AS: \( D=\bigcup T \)
moreover
from AS, assms(2) have \( \{\bigcup T\}\subseteq DualBase B T \) using DualBase_def
moreover have \( \bigcup T = \bigcap \{\bigcup T\} \)
ultimately have \( thesis \) using K
We have already seen for a base that whenever there is a union of open sets, we can consider only basic open sets due to the fact that any open set is a union of basic open sets. What we should expect now is that when there is an intersection of closed sets, we can consider only dual basic closed sets.
lemma closure_dual_base:
assumes \( U \text{ is a base for } Q \), \( Q\text{ is a topology } \), \( A\subseteq \bigcup Q \)
shows \( \text{Closure}(A,Q)=\bigcap \{T\in DualBase U Q.\ A\subseteq T\} \)proof from assms(1) have T: \( \bigcup Q\in DualBase U Q \) using DualBase_def
moreover {
}
{
fix \( T \)
assume A: \( T\in DualBase U Q \), \( A\subseteq T \)
with assms(1) obtain \( R \) where \( (T=\bigcup Q-R\wedge R\in U)\vee T=\bigcup Q \) using DualBase_def
with A(2), assms(1,2) have \( (T\text{ is closed in }Q) \), \( A\subseteq T \), \( T\in Pow(\bigcup Q) \) using Top_3_L1, topology0_def, Top_3_L9, base_sets_open
then have SUB: \( \{T\in DualBase U Q.\ A\subseteq T\}\subseteq \{T\in Pow(\bigcup Q).\ (T\text{ is closed in }Q)\wedge A\subseteq T\} \)
ultimately have \( \bigcap \{T\in Pow(\bigcup Q).\ (T\text{ is closed in }Q)\wedge A\subseteq T\}\subseteq \bigcap \{T\in DualBase U Q.\ A\subseteq T\} \) using assms(3)
then show \( \text{Closure}(A,Q)\subseteq \bigcap \{T\in DualBase U Q.\ A\subseteq T\} \) using Closure_def, ClosedCovers_def
fix \( x \)
assume A: \( x\in \bigcap \{T\in DualBase U Q.\ A\subseteq T\} \)
{
fix \( T \)
assume B: \( x\in T \), \( T\in U \)
{
assume C: \( A\cap T=0 \)
from B(2), assms(1) have \( \bigcup Q-T\in DualBase U Q \) using DualBase_def
moreover
from C, assms(3) have \( A\subseteq \bigcup Q-T \)
moreover from B(1) have \( x\notin \bigcup Q-T \)
ultimately have \( x\notin \bigcap \{T\in DualBase U Q.\ A\subseteq T\} \)
with A have \( False \)
hence \( A\cap T\neq 0 \)
hence \( \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0 \)
moreover
from T, A, assms(3) have \( x\in \bigcup Q \)
ultimately have \( x\in \text{Closure}(A,Q) \) using closure_set_base_topology, assms
thus \( \bigcap \{T \in DualBase U Q .\ A \subseteq T\} \subseteq \text{Closure}(A, Q) \)
qed
Partition topology
In the theory file Partitions\_ZF.thy; there is a definition to work with partitions. In this setting is much easier to work with a family of subsets.
A partition of a set \(X\) is a family of pairwise disjoint nonempty subsets whose union covers all of \(X\).
definition
\( (U \text{ is a partition of } X) \equiv (\bigcup U=X \wedge (\forall A\in U.\ \forall B\in U.\ A=B\vee A\cap B=0)\wedge 0\notin U) \)
A subcollection of a partition is a partition of its union.
lemma subpartition:
assumes \( U \text{ is a partition of } X \), \( V\subseteq U \)
shows \( V\text{ is a partition of }\bigcup V \) using assms unfolding IsAPartition_defA restriction of a partition is a partition. If the empty set appears it has to be removed.
lemma restriction_partition:
assumes \( U \text{ is a partition of }X \)
shows \( ((U \text{ restricted to } Y)-\{0\}) \text{ is a partition of } (X\cap Y) \) using assms unfolding IsAPartition_def, RestrictedTo_defGiven a partition, the complement of a union of a subfamily is a union of a subfamily.
lemma diff_union_is_union_diff:
assumes \( R\subseteq P \), \( P \text{ is a partition of } X \)
shows \( X - \bigcup R=\bigcup (P-R) \)proof{
}
}
}
fix \( x \)
assume \( x\in X - \bigcup R \)
hence P: \( x\in X \), \( x\notin \bigcup R \)
{
fix \( T \)
assume \( T\in R \)
with P(2) have \( x\notin T \)
with P(1), assms(2) obtain \( Q \) where \( Q\in (P-R) \), \( x\in Q \) using IsAPartition_def
hence \( x\in \bigcup (P-R) \)
thus \( X - \bigcup R\subseteq \bigcup (P-R) \)
{
fix \( x \)
assume \( x\in \bigcup (P-R) \)
then obtain \( Q \) where \( Q\in P-R \), \( x\in Q \)
hence C: \( Q\in P \), \( Q\notin R \), \( x\in Q \)
then have \( x\in \bigcup P \)
with assms(2) have \( x\in X \) using IsAPartition_def
moreover {
}
assume \( x\in \bigcup R \)
then obtain \( t \) where G: \( t\in R \), \( x\in t \)
with C(3), assms(1) have \( t\cap Q\neq 0 \), \( t\in P \)
with assms(2), C(1,3) have \( t=Q \) using IsAPartition_def
with C(2), G(1) have \( False \)
hence \( x\notin \bigcup R \)
ultimately have \( x\in X-\bigcup R \)
thus \( \bigcup (P-R)\subseteq X - \bigcup R \)
qed
Partition topology is a topology.
A partition satisfies the base condition.
A partition satisfies the base condition because any two distinct partition classes are either equal or disjoint, so their intersection is trivially covered by a partition class.
lemma partition_base_condition:
assumes \( P \text{ is a partition of } X \)
shows \( P \text{ satisfies the base condition } \)proof{
}
}
fix \( U \) \( V \)
assume AS: \( U\in P\wedge V\in P \)
with assms have A: \( U=V\vee U\cap V=0 \) using IsAPartition_def
{
fix \( x \)
assume ASS: \( x\in U\cap V \)
with A have \( U=V \)
with AS, ASS have \( U\in P \), \( x\in U\wedge U\subseteq U\cap V \)
hence \( \exists W\in P.\ x\in W\wedge W\subseteq U\cap V \)
hence \( (\forall x \in U\cap V.\ \exists W\in P.\ x\in W \wedge W \subseteq U\cap V) \)
then show \( thesis \) using SatisfiesBaseCondition_def
qed
Since a partition is a base of a topology, and this topology is uniquely determined; we can built it. In the definition we have to make sure that we have a partition.
definition
\( (U \text{ is a partition of } X) \Longrightarrow PTopology X U \equiv TopologyBase U \)
The partition topology is indeed a topology, and the partition is a base for it.
theorem Ptopology_is_a_topology:
assumes \( U \text{ is a partition of } X \)
shows \( (PTopology X U) \text{ is a topology } \) and \( U \text{ is a base for } (PTopology X U) \) using assms, Base_topology_is_a_topology, partition_base_condition, PartitionTopology_defThe partition topology satisfies the assumptions of the topology0 locale.
lemma topology0_ptopology:
assumes \( U \text{ is a partition of } X \)
shows \( topology0(PTopology X U) \) using Ptopology_is_a_topology, topology0_def, assmsThe union of all open sets in the partition topology equals the set \(X\) that the partition covers.
lemma union_ptopology:
assumes \( U \text{ is a partition of } X \)
shows \( \bigcup (PTopology X U)=X \) using assms, Ptopology_is_a_topology(2), Top_1_2_L5, IsAPartition_defThe closed sets are the open sets.
lemma closed_sets_ptopology:
assumes \( T \text{ is a partition of } X \)
shows \( D \text{ is closed in } (PTopology X T) \longleftrightarrow D\in (PTopology X T) \)proof from assms have B: \( T\text{ is a base for }(PTopology X T) \) using Ptopology_is_a_topology(2)
{
fix \( D \)
assume \( D \text{ is closed in } (PTopology X T) \)
with assms have A: \( D\in Pow(X) \), \( X-D\in (PTopology X T) \) using IsClosed_def, union_ptopology
from A(2), B have \( \exists A\in Pow(T).\ X \setminus D = \bigcup A \) using Top_1_2_L1
then obtain \( R \) where Q: \( R\subseteq T \), \( X-D=\bigcup R \)
from A(1) have \( X-(X-D)=D \)
with Q(2) have \( D=X-\bigcup R \)
with Q(1), assms have \( D=\bigcup (T-R) \) using diff_union_is_union_diff
with B show \( D\in (PTopology X T) \) using IsAbaseFor_def
fix \( D \)
assume \( D\in (PTopology X T) \)
with B obtain \( R \) where Q: \( R\subseteq T \), \( D=\bigcup R \) using IsAbaseFor_def
hence \( X-D=X-\bigcup R \)
with Q(1), assms have \( X-D=\bigcup (T-R) \) using diff_union_is_union_diff
with B have \( X-D\in (PTopology X T) \) using IsAbaseFor_def
moreover
from Q have \( D\subseteq \bigcup T \)
with assms have \( D\subseteq X \) using IsAPartition_def
ultimately show \( D\text{ is closed in } (PTopology X T) \) using IsClosed_def, assms, union_ptopology
There is a formula for the interior given by an intersection of sets of the dual base. Is the intersection of all the closed sets of the dual basis such that they do not complement \(A\) to \(X\). Since the interior of \(X\) must be inside \(X\), we have to enter \(X\) as one of the sets to be intersected.
lemma interior_set_ptopology:
assumes \( U \text{ is a partition of } X \), \( A\subseteq X \)
shows \( \text{Interior}(A,(PTopology X U))=\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \)proof{
}
}
}
}
}
}
}
}
fix \( x \)
assume \( x\in \text{Interior}(A,(PTopology X U)) \)
with assms obtain \( R \) where A: \( x\in R \), \( R\in (PTopology X U) \), \( R\subseteq A \) using open_open_neigh, topology0_ptopology, Top_2_L2, Top_2_L1
with assms obtain \( B \) where B: \( B\subseteq U \), \( R=\bigcup B \) using Ptopology_is_a_topology(2), IsAbaseFor_def
from A(1,3), assms have XX: \( x\in X \), \( X\in \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \) using union_ptopology, DualBase_def, Ptopology_is_a_topology(2)
from B(2), A(1) obtain \( S \) where C: \( S\in B \), \( x\in S \)
{
fix \( T \)
assume AS: \( T\in DualBase U (PTopology X U) \), \( T \cup A\neq X \)
from AS(1), assms obtain \( w \) where \( (T=X-w\wedge w\in U)\vee (T=X) \) using DualBase_def, union_ptopology, Ptopology_is_a_topology(2)
with assms(2), AS(2) have D: \( T=X-w \), \( w\in U \)
from D(2) have wU: \( w\subseteq \bigcup U \)
from assms(1) have \( U \text{ is a base for }(PTopology X U) \) using Ptopology_is_a_topology(2)
then have \( \bigcup U=\bigcup (PTopology X U) \) using Top_1_2_L5
with wU have \( w\subseteq \bigcup (PTopology X U) \)
with assms(1) have \( w\subseteq X \) using union_ptopology
with D(1) have \( X-T=w \)
with D(2) have \( X-T\in U \)
{
assume \( x\in X-T \)
with C, B(1) have \( S\in U \), \( S\cap (X-T)\neq 0 \)
with \( X-T\in U \), assms(1) have \( X-T=S \) using IsAPartition_def
with \( X-T=w \), \( T=X-w \) have \( X-S=T \)
with AS(2) have \( X-S\cup A\neq X \)
from A(3), B(2), C(1) have \( S\subseteq A \)
hence \( X-A\subseteq X-S \)
with assms(2) have \( X-S\cup A=X \)
with \( X-S\cup A\neq X \) have \( False \)
then have \( x\in T \) using XX
with XX have \( x\in \bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \)
thus \( \text{Interior}(A,(PTopology X U))\subseteq \bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \)
{
fix \( x \)
assume p: \( x\in \bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \)
hence noE: \( \bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\}\neq 0 \)
{
fix \( T \)
assume \( T\in DualBase U (PTopology X U) \)
with assms(1) obtain \( w \) where \( T=X\vee (w\in U\wedge T=X-w) \) using DualBase_def, Ptopology_is_a_topology(2), union_ptopology
with assms(1) have I: \( T=X\vee (w\in (PTopology X U)\wedge T=X-w) \) using base_sets_open, Ptopology_is_a_topology(2)
{
assume \( T=X \)
with assms(1) have A: \( T=\bigcup (PTopology X U) \) using union_ptopology
from assms(1) have B: \( (\bigcup (PTopology X U)) \text{ is closed in }(PTopology X U) \) using topology0_ptopology, Top_3_L1
from A, B have \( T \text{ is closed in }(PTopology X U) \)
moreover {
}
ultimately have \( T\text{ is closed in }(PTopology X U) \) using I
assume as: \( w\in (PTopology X U) \), \( T=X-w \)
have X: \( X=\bigcup (PTopology X U) \) using union_ptopology, assms(1)
from as(1), assms(1) have \( (\bigcup (PTopology X U) -w) \text{ is closed in } (PTopology X U) \) using topology0_ptopology, Top_3_L9
with X, as(2) have \( T \text{ is closed in }(PTopology X U) \)
then have \( \forall T\in (DualBase U (PTopology X U)).\ T \text{ is closed in }(PTopology X U) \)
moreover
from assms(1), p have \( X\in \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \) and X: \( x\in X \) using Ptopology_is_a_topology(2), DualBase_def, union_ptopology
then have \( \{T \in DualBase U PTopology X U .\ \)
\( T = X \vee T \cup A \neq X\} \neq \emptyset \)
ultimately have \( (\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\}) \text{ is closed in }(PTopology X U) \) using Top_3_L4, topology0_ptopology, assms(1)
with assms(1) have ab: \( (\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\})\in (PTopology X U) \) using closed_sets_ptopology
with assms(1) obtain \( B \) where \( B\in Pow(U) \), \( (\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\})=\bigcup B \) using Ptopology_is_a_topology(2), IsAbaseFor_def
with p obtain \( R \) where R: \( x\in R \), \( R\in U \), \( R\subseteq (\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\}) \)
from assms(1) have base: \( U \text{ is a base for } (PTopology X U) \) using Ptopology_is_a_topology(2)
from base, R(2) have R2: \( R\in (PTopology X U) \) using base_sets_open
from base, assms(1), R(2) have \( X-R\in DualBase U (PTopology X U) \) using union_ptopology, DualBase_def
with assms(1), R(1,3), R2 have R: \( x\in R \), \( R\in (PTopology X U) \), \( R\subseteq (\bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\}) \), \( X-R\in DualBase U (PTopology X U) \)
{
assume \( (X-R) \cup A\neq X \)
with R(4) have \( X-R\in \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\} \)
hence \( \bigcap \{T\in DualBase U (PTopology X U).\ T=X\vee T\cup A\neq X\}\subseteq X-R \)
with R(3) have \( R\subseteq X-R \) using subset_trans
hence \( R=0 \)
with R(1) have \( False \)
hence I: \( (X-R) \cup A=X \)
{
fix \( y \)
assume ASR: \( y\in R \)
with R(2) have \( y\in \bigcup (PTopology X U) \)
with assms(1) have XX: \( y\in X \) using union_ptopology
with I have \( y\in (X-R) \cup A \)
with XX have \( y\notin R\vee y\in A \)
with ASR have \( y\in A \)
hence \( R\subseteq A \)
with R(1,2) have \( \exists R\in (PTopology X U).\ (x\in R\wedge R\subseteq A) \)
with assms(1) have \( x\in \text{Interior}(A,(PTopology X U)) \) using Top_2_L6, topology0_ptopology
thus \( \bigcap \{T \in DualBase U PTopology X U .\ T = X \vee T \cup A \neq X\} \subseteq \text{Interior}(A, PTopology X U) \)
qed
The closure of a set is the union of all the sets of the partition which intersect with A.
lemma closure_set_ptopology:
assumes \( U \text{ is a partition of } X \), \( A\subseteq X \)
shows \( \text{Closure}(A,(PTopology X U))=\bigcup \{T\in U.\ T\cap A\neq 0\} \)proof from assms(1) have t: \( \bigcup (PTopology X U) =\bigcup U \) using Top_1_2_L5, Ptopology_is_a_topology(2)
{
fix \( x \)
assume A: \( x\in \text{Closure}(A,(PTopology X U)) \)
from assms(2) have I: \( A\subseteq \bigcup (PTopology X U) \) using assms(1), union_ptopology
from assms(1) have t0: \( topology0(PTopology X U) \) using topology0_ptopology
with A, I have I: \( x\in \bigcup (PTopology X U) \) using Top_3_L11(1)
from t, I have \( x\in \bigcup U \)
then obtain \( W \) where B: \( x\in W \), \( W\in U \)
with A have \( x\in \text{Closure}(A,(PTopology X U))\cap W \)
moreover
from B(2) have \( W\in (PTopology X U) \) using base_sets_open, Ptopology_is_a_topology(2), assms(1)
ultimately have \( A\cap W\neq 0 \) using t0, assms, cl_inter_neigh, union_ptopology
with B have \( x\in \bigcup \{T\in U.\ T\cap A\neq 0\} \)
thus \( \text{Closure}(A, PTopology X U) \subseteq \bigcup \{T \in U .\ T \cap A \neq 0\} \)
{
fix \( x \)
assume \( x\in \bigcup \{T \in U .\ T \cap A \neq 0\} \)
then obtain \( T \) where A: \( x\in T \), \( T\in U \), \( T\cap A\neq 0 \)
from assms have \( A\subseteq \bigcup (PTopology X U) \) using union_ptopology
moreover
}
from A(1,2) have \( x\in \bigcup (PTopology X U) \) using t
moreover {
fix \( Q \)
assume B: \( Q\in (PTopology X U) \), \( x\in Q \)
with assms(1) obtain \( M \) where C: \( Q=\bigcup M \), \( M\subseteq U \) using Ptopology_is_a_topology(2), IsAbaseFor_def
from B(2), C(1) obtain \( R \) where D: \( R\in M \), \( x\in R \)
with C(2), A(1,2) have \( R\cap T\neq 0 \), \( R\in U \), \( T\in U \)
with assms(1) have \( R=T \) using IsAPartition_def
with C(1), D(1) have \( T\subseteq Q \)
with A(3) have \( Q\cap A\neq 0 \)
then have \( \forall Q\in (PTopology X U).\ x\in Q \longrightarrow Q\cap A\neq 0 \)
ultimately have \( x\in \text{Closure}(A,(PTopology X U)) \) using inter_neigh_cl, assms(1), topology0_ptopology
then show \( \bigcup \{T \in U .\ T \cap A \neq 0\} \subseteq \text{Closure}(A, PTopology X U) \)
qed
The boundary of a set is given by the union of the sets of the partition which have non empty intersection with the set but that are not fully contained in it. Another equivalent statement would be: the union of the sets of the partition which have non empty intersection with the set and its complement.
lemma boundary_set_ptopology:
assumes \( U \text{ is a partition of } X \), \( A\subseteq X \)
shows \( \text{Boundary}(A,(PTopology X U))=\bigcup \{T\in U.\ T\cap A\neq 0 \wedge \neg (T\subseteq A)\} \)proof from assms have \( \text{Closure}(A,(PTopology X U))=\bigcup \{T \in U .\ T \cap A \neq 0\} \) using closure_set_ptopology
moreover
from assms(1) have \( \text{Interior}(A,(PTopology X U))=\bigcup \{T \in U .\ T \subseteq A\} \) using interior_set_base_topology, Ptopology_is_a_topology
ultimately have A: \( \text{Boundary}(A,(PTopology X U))=\bigcup \{T \in U .\ T \cap A \neq 0\} - \bigcup \{T \in U .\ T \subseteq A\} \) using assms, Top_3_L12, topology0_ptopology, union_ptopology
from assms(1) have \( (\{T \in U .\ T \cap A \neq 0\}) \text{ is a partition of } \bigcup (\{T \in U .\ T \cap A \neq 0\}) \) using subpartition
moreover {
}
fix \( T \)
assume \( T\in U \), \( T\subseteq A \)
with assms(1) have \( T\cap A=T \), \( T\neq 0 \) using IsAPartition_def
with \( T\in U \) have \( T\cap A\neq 0 \), \( T\in U \)
then have \( \{T \in U .\ T \subseteq A\}\subseteq \{T \in U .\ T \cap A \neq 0\} \)
ultimately have \( \bigcup \{T \in U .\ T \cap A \neq 0\} - \bigcup \{T \in U .\ T \subseteq A\}=\bigcup ((\{T \in U .\ T \cap A \neq 0\})-(\{T \in U .\ T \subseteq A\})) \) using diff_union_is_union_diff
also
qed
have \( \ldots =\bigcup (\{T \in U .\ T \cap A \neq 0 \wedge \neg (T\subseteq A)\}) \)
finally show \( thesis \) using A
Special cases and subspaces
The discrete and the indiscrete topologies appear as special cases of this partition topologies.
The singletons \(\{x\}\) for \(x \in X\) form a partition of \(X\).
lemma discrete_partition:
shows \( \{\{x\}.\ x\in X\} \text{ is a partition of }X \) using IsAPartition_defFor a nonempty set \(X\), the family \(\{X\}\) consisting only of \(X\) itself is a partition of \(X\).
lemma indiscrete_partition:
assumes \( X\neq 0 \)
shows \( \{X\} \text{ is a partition of } X \) using assms, IsAPartition_defThe partition topology arising from the discrete partition (singletons) equals the discrete topology \(\mathrm{Pow}(X)\).
theorem discrete_ptopology:
shows \( (PTopology X \{\{x\}.\ x\in X\})=Pow(X) \)proof{
}
}
fix \( t \)
assume \( t\in (PTopology X \{\{x\}.\ x\in X\}) \)
hence \( t\subseteq \bigcup (PTopology X \{\{x\}.\ x\in X\}) \)
then have \( t\in Pow(X) \) using union_ptopology, discrete_partition
thus \( (PTopology X \{\{x\}.\ x\in X\})\subseteq Pow(X) \)
{
fix \( t \)
assume A: \( t\in Pow(X) \)
have \( \bigcup (\{\{x\}.\ x\in t\})=t \)
moreover
from A have \( \{\{x\}.\ x\in t\}\in Pow(\{\{x\}.\ x\in X\}) \)
hence \( \bigcup (\{\{x\}.\ x\in t\})\in \{\bigcup A .\ A \in Pow(\{\{x\} .\ x \in X\})\} \)
ultimately have \( t\in (PTopology X \{\{x\} .\ x \in X\}) \) using Ptopology_is_a_topology(2), discrete_partition, IsAbaseFor_def
thus \( Pow(X) \subseteq (PTopology X \{\{x\} .\ x \in X\}) \)
qed
The partition topology arising from the indiscrete partition \(\{X\}\) equals the indiscrete topology \(\{0, X\}\).
theorem indiscrete_ptopology:
assumes \( X\neq 0 \)
shows \( (PTopology X \{X\})=\{0,X\} \)proof{
}
fix \( T \)
assume \( T\in (PTopology X \{X\}) \)
with assms obtain \( M \) where \( M\subseteq \{X\} \), \( \bigcup M=T \) using Ptopology_is_a_topology(2), indiscrete_partition, IsAbaseFor_def
then have \( T=0\vee T=X \)
then show \( (PTopology X \{X\})\subseteq \{0,X\} \)
from assms have \( 0\in (PTopology X \{X\}) \) using Ptopology_is_a_topology(1), empty_open, indiscrete_partition
moreover
qed
from assms have \( \bigcup (PTopology X \{X\})\in (PTopology X \{X\}) \) using union_open, Ptopology_is_a_topology(1), indiscrete_partition
with assms have \( X\in (PTopology X \{X\}) \) using union_ptopology, indiscrete_partition
ultimately show \( \{0,X\}\subseteq (PTopology X \{X\}) \)
The topological subspaces of the \( (PTopology X U) \) are partition topologies.
lemma subspace_ptopology:
assumes \( U\text{ is a partition of }X \)
shows \( (PTopology X U) \text{ restricted to } Y=(PTopology (X\cap Y) ((U \text{ restricted to } Y)-\{0\})) \)proof from assms have \( U\text{ is a base for }(PTopology X U) \) using Ptopology_is_a_topology(2)
then have \( (U\text{ restricted to } Y)\text{ is a base for }(PTopology X U)\text{ restricted to } Y \) using subspace_base_topology
then have \( ((U\text{ restricted to } Y)-\{0\})\text{ is a base for }(PTopology X U)\text{ restricted to } Y \) using base_no_0
moreover
qed
from assms have \( ((U\text{ restricted to } Y)-\{0\}) \text{ is a partition of } (X\cap Y) \) using restriction_partition
then have \( ((U\text{ restricted to } Y)-\{0\})\text{ is a base for }(PTopology (X\cap Y) ((U \text{ restricted to } Y)-\{0\})) \) using Ptopology_is_a_topology(2)
ultimately show \( thesis \) using same_base_same_top
Order topologies
Given a totally ordered set, several topologies can be defined using the order relation. First we define an open interval, notice that the set defined as Interval is a closed interval; and open rays.
An open interval in the ordered set \((X,r)\) is the closed interval with both endpoints removed.
definition
\( \text{IntervalX}(X,r,b,c)\equiv ( \text{Interval}(r,b,c)\cap X)-\{b,c\} \)
A left open ray consists of all points of \(X\) that are strictly below a given bound.
definition
\( \text{LeftRayX}(X,r,b)\equiv \{c\in X.\ \langle c,b\rangle \in r\}-\{b\} \)
A right open ray consists of all points of \(X\) that are strictly above a given bound.
definition
\( \text{RightRayX}(X,r,b)\equiv \{c\in X.\ \langle b,c\rangle \in r\}-\{b\} \)
Intersections of intervals and rays.
lemma inter_two_intervals:
assumes \( bu\in X \), \( bv\in X \), \( cu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{IntervalX}(X,r,bu,cu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \)proof{
}
}
fix \( x \)
assume ASS: \( x\in \text{IntervalX}(X,r,bu,cu)\cap \text{IntervalX}(X,r,bv,cv) \)
then have \( x\in \text{IntervalX}(X,r,bu,cu) \), \( x\in \text{IntervalX}(X,r,bv,cv) \)
then have BB: \( x\in X \), \( x\in \text{Interval}(r,bu,cu) \), \( x\neq bu \), \( x\neq cu \), \( x\in \text{Interval}(r,bv,cv) \), \( x\neq bv \), \( x\neq cv \) using IntervalX_def, assms
have RR: \( \langle bu,x\rangle \in r \), \( \langle x,cu\rangle \in r \), \( \langle bv,x\rangle \in r \), \( \langle x,cv\rangle \in r \) using BB(2,5), Order_ZF_2_L1A
{
{
}
}
assume \( \langle bu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,bu,bv) = bv \) unfolding GreaterOf_def
with RR(3) have \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
moreover {
}
ultimately have I: \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
assume \( \langle bu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,bu,bv) = bu \) unfolding GreaterOf_def
with RR(1) have \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
then have I: \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
{
{
}
}
assume \( \langle cu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,cu,cv) = cu \) unfolding SmallerOf_def
with RR(2) have \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \)
moreover {
}
ultimately have II: \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \)
assume \( \langle cu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,cu,cv) = cv \) unfolding SmallerOf_def
with RR(4) have \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \)
then have II: \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \)
from BB have \( x\in X \)
moreover
have \( x\neq \text{GreaterOf}(r,bu,bv) \) using GreaterOf_def, BB(6,3)
moreover have \( x\neq \text{SmallerOf}(r,cu,cv) \) using SmallerOf_def, BB(7,4)
moreover from I, II have \( x\in \text{Interval}(r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \) using Order_ZF_2_L1
ultimately have \( x\in \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \) using IntervalX_def
then show \( \text{IntervalX}(X, r, bu, cu) \cap \text{IntervalX}(X, r, bv, cv) \subseteq \text{IntervalX}(X, r, \text{GreaterOf}(r, bu, bv), \text{SmallerOf}(r, cu, cv)) \)
{
fix \( x \)
assume \( x\in \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \)
then have BB: \( x\in X \), \( x\in \text{Interval}(r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \), \( x\neq \text{GreaterOf}(r,bu,bv) \), \( x\neq \text{SmallerOf}(r,cu,cv) \) using IntervalX_def
from BB(2) have CC: \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \), \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \) using Order_ZF_2_L1A
from BB have \( x\in X \)
moreover {
{
}
}
moreover {
assume AS: \( \langle bu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,bu,bv)=bv \) using GreaterOf_def
then have A: \( \langle bv,x\rangle \in r \) using CC(1)
with AS have \( \langle bu,x\rangle \in r \) using assms(5) unfolding IsLinOrder_def, trans_def
with A have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
moreover {
}
ultimately have R: \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
assume AS: \( \langle bu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,bu,bv)=bu \) using GreaterOf_def
then have A: \( \langle bu,x\rangle \in r \) using CC(1)
from AS have \( \langle bv,bu\rangle \in r \) using assms, IsLinOrder_def, IsTotal_def, assms
with A have \( \langle bv,x\rangle \in r \) using assms(5) unfolding IsLinOrder_def, trans_def
with A have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \), \( x\neq bu \), \( x\neq bv \)
assume AS: \( x=bu \)
then have \( \langle bv,bu\rangle \in r \) using R(2)
then have \( \text{GreaterOf}(r,bu,bv)=bu \) using GreaterOf_def, assms, IsLinOrder_def, antisym_def
then have \( False \) using AS, BB(3)
assume AS: \( x=bv \)
then have \( \langle bu,bv\rangle \in r \) using R(1)
then have \( \text{GreaterOf}(r,bu,bv)=bv \) using GreaterOf_def
then have \( False \) using AS, BB(3)
{
}
}
ultimately have \( x\in \text{IntervalX}(X,r,bu,cu) \), \( x\in \text{IntervalX}(X,r,bv,cv) \) using Order_ZF_2_L1, IntervalX_def, assms
assume AS: \( \langle cu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,cu,cv)=cu \) using SmallerOf_def
then have A: \( \langle x,cu\rangle \in r \) using CC(2)
with AS have \( \langle x,cv\rangle \in r \) using assms(5) unfolding IsLinOrder_def, trans_def
with A have \( \langle x,cu\rangle \in r \), \( \langle x,cv\rangle \in r \)
moreover {
}
ultimately have R: \( \langle x,cv\rangle \in r \), \( \langle x,cu\rangle \in r \)
assume AS: \( \langle cu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,cu,cv)=cv \) using SmallerOf_def
then have A: \( \langle x,cv\rangle \in r \) using CC(2)
from AS have \( \langle cv,cu\rangle \in r \) using assms, IsLinOrder_def, IsTotal_def
with A have \( \langle x,cu\rangle \in r \) using assms(5) unfolding IsLinOrder_def, trans_def
with A have \( \langle x,cv\rangle \in r \), \( \langle x,cu\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle x,cu\rangle \in r \), \( \langle x,cv\rangle \in r \), \( x\neq cu \), \( x\neq cv \)
assume AS: \( x=cv \)
then have \( \langle cv,cu\rangle \in r \) using R(2)
then have \( \text{SmallerOf}(r,cu,cv)=cv \) using SmallerOf_def, assms, IsLinOrder_def, antisym_def
then have \( False \) using AS, BB(4)
assume AS: \( x=cu \)
then have \( \langle cu,cv\rangle \in r \) using R(1)
then have \( \text{SmallerOf}(r,cu,cv)=cu \) using SmallerOf_def
then have \( False \) using AS, BB(4)
then have \( x\in \text{IntervalX}(X, r, bu, cu) \cap \text{IntervalX}(X, r, bv, cv) \)
then show \( \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \subseteq \text{IntervalX}(X, r, bu, cu) \cap \text{IntervalX}(X, r, bv, cv) \)
qed
The intersection of a right ray with an open interval is again an open interval, with the left endpoint replaced by the greater of the two lower bounds.
lemma inter_rray_interval:
assumes \( bv\in X \), \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{RightRayX}(X,r,bu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv),cv) \)proof{
}
}
}
fix \( x \)
assume \( x\in \text{RightRayX}(X,r,bu)\cap \text{IntervalX}(X,r,bv,cv) \)
then have \( x\in \text{RightRayX}(X,r,bu) \), \( x\in \text{IntervalX}(X,r,bv,cv) \)
then have BB: \( x\in X \), \( x\neq bu \), \( x\neq bv \), \( x\neq cv \), \( \langle bu,x\rangle \in r \), \( x\in \text{Interval}(r,bv,cv) \) using RightRayX_def, IntervalX_def
then have A: \( \langle bv,x\rangle \in r \), \( \langle x,cv\rangle \in r \) using Order_ZF_2_L1A
{
assume \( \langle bu,bv\rangle \in r \)
then have g: \( \text{GreaterOf}(r,bu,bv) = bv \) unfolding GreaterOf_def
with A(1) have \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
moreover {
}
ultimately have \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
assume \( \langle bu,bv\rangle \notin r \)
then have g: \( \text{GreaterOf}(r,bu,bv) = bu \) unfolding GreaterOf_def
with BB(5) have \( \langle \text{GreaterOf}(r,bu,bv),x\rangle \in r \)
with \( \langle x,cv\rangle \in r \) have \( x\in \text{Interval}(r, \text{GreaterOf}(r,bu,bv),cv) \) using Order_ZF_2_L1
then have \( x\in \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv),cv) \) using BB(1-4), IntervalX_def, GreaterOf_def
then show \( \text{RightRayX}(X, r, bu) \cap \text{IntervalX}(X, r, bv, cv) \subseteq \text{IntervalX}(X, r, \text{GreaterOf}(r, bu, bv), cv) \)
{
fix \( x \)
assume \( x\in \text{IntervalX}(X, r, \text{GreaterOf}(r, bu, bv), cv) \)
then have BB: \( x\in X \), \( x\in \text{Interval}(r, \text{GreaterOf}(r, bu, bv), cv) \), \( x\neq cv \), \( x\neq \text{GreaterOf}(r, bu, bv) \) using IntervalX_def
then have R: \( \langle \text{GreaterOf}(r, bu, bv),x\rangle \in r \), \( \langle x,cv\rangle \in r \) using Order_ZF_2_L1A
with \( x\neq cv \) have \( \langle x,cv\rangle \in r \), \( x\neq cv \)
moreover {
{
}
}
ultimately have \( x\in \text{RightRayX}(X, r, bu) \), \( x\in \text{IntervalX}(X, r, bv, cv) \) unfolding RightRayX_def, IntervalX_def using Order_ZF_2_L1, BB(1)
assume AS: \( \langle bu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,bu,bv)=bv \) using GreaterOf_def
then have I: \( \langle bv,x\rangle \in r \) using R(1)
with AS have \( \langle bu,x\rangle \in r \) using assms(4) unfolding IsLinOrder_def, trans_def
with I have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
moreover {
}
ultimately have T: \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
assume AS: \( \langle bu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,bu,bv)=bu \) using GreaterOf_def
then have I: \( \langle bu,x\rangle \in r \) using R(1)
from AS have \( \langle bv,bu\rangle \in r \) using assms unfolding IsLinOrder_def, IsTotal_def
with I have \( \langle bv,x\rangle \in r \) using assms(4) unfolding IsLinOrder_def, trans_def
with I have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle bu,x\rangle \in r \), \( \langle bv,x\rangle \in r \), \( x\neq bu \), \( x\neq bv \)
assume AS: \( x=bu \)
then have \( \langle bv,bu\rangle \in r \) using T(2)
then have \( \text{GreaterOf}(r,bu,bv)=bu \) using assms unfolding GreaterOf_def, IsLinOrder_def, antisym_def
with \( x\neq \text{GreaterOf}(r,bu,bv) \) have \( False \) using AS
assume AS: \( x=bv \)
then have \( \langle bu,bv\rangle \in r \) using T(1)
then have \( \text{GreaterOf}(r,bu,bv)=bv \) unfolding GreaterOf_def
with \( x\neq \text{GreaterOf}(r,bu,bv) \) have \( False \) using AS
then have \( x\in \text{RightRayX}(X, r, bu) \cap \text{IntervalX}(X, r, bv, cv) \)
then show \( \text{IntervalX}(X, r, \text{GreaterOf}(r, bu, bv), cv) \subseteq \text{RightRayX}(X, r, bu) \cap \text{IntervalX}(X, r, bv, cv) \)
qed
The intersection of a left ray with an open interval is again an open interval, with the right endpoint replaced by the smaller of the two upper bounds.
lemma inter_lray_interval:
assumes \( bv\in X \), \( cu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,cu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r,bv, \text{SmallerOf}(r,cu,cv)) \)proof{
}
}
fix \( x \)
assume \( x\in \text{LeftRayX}(X,r,cu)\cap \text{IntervalX}(X,r,bv,cv) \)
then have B: \( x\neq cu \), \( x\in X \), \( \langle x,cu\rangle \in r \), \( \langle bv,x\rangle \in r \), \( \langle x,cv\rangle \in r \), \( x\neq bv \), \( x\neq cv \) unfolding LeftRayX_def, IntervalX_def, Interval_def
from \( \langle x,cu\rangle \in r \), \( \langle x,cv\rangle \in r \) have C: \( \langle x, \text{SmallerOf}(r, cu, cv)\rangle \in r \) using SmallerOf_def
from B(7,1) have \( x\neq \text{SmallerOf}(r,cu,cv) \) using SmallerOf_def
then have \( x\in \text{IntervalX}(X,r,bv, \text{SmallerOf}(r,cu,cv)) \) using B, C, IntervalX_def, Order_ZF_2_L1
then show \( \text{LeftRayX}(X, r, cu) \cap \text{IntervalX}(X, r, bv, cv) \subseteq \text{IntervalX}(X, r, bv, \text{SmallerOf}(r, cu, cv)) \)
{
fix \( x \)
assume \( x\in \text{IntervalX}(X,r,bv, \text{SmallerOf}(r,cu,cv)) \)
then have R: \( x\in X \), \( \langle bv,x\rangle \in r \), \( \langle x, \text{SmallerOf}(r,cu,cv)\rangle \in r \), \( x\neq bv \), \( x\neq \text{SmallerOf}(r,cu,cv) \) using IntervalX_def, Interval_def
then have \( \langle bv,x\rangle \in r \), \( x\neq bv \)
moreover {
{
}
}
moreover assume AS: \( \langle cu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,cu,cv)=cu \) using SmallerOf_def
then have xcu: \( \langle x,cu\rangle \in r \) using R(3)
with AS have \( \langle x,cv\rangle \in r \) using assms(4) unfolding IsLinOrder_def, trans_def
with xcu have \( \langle x,cu\rangle \in r \), \( \langle x,cv\rangle \in r \)
moreover {
}
ultimately have T: \( \langle x,cv\rangle \in r \), \( \langle x,cu\rangle \in r \)
assume AS: \( \langle cu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,cu,cv)=cv \) using SmallerOf_def
then have xcv: \( \langle x,cv\rangle \in r \) using R(3)
from AS have \( \langle cv,cu\rangle \in r \) using assms, IsLinOrder_def, IsTotal_def, assms
with xcv have \( \langle x,cu\rangle \in r \) using assms(4) unfolding IsLinOrder_def, trans_def
with xcv have \( \langle x,cv\rangle \in r \), \( \langle x,cu\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle x,cu\rangle \in r \), \( \langle x,cv\rangle \in r \), \( x\neq cu \), \( x\neq cv \)
assume AS: \( x=cu \)
then have \( \langle cu,cv\rangle \in r \) using T(1)
then have \( \text{SmallerOf}(r,cu,cv)=cu \) using SmallerOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(5) have \( False \)
assume AS: \( x=cv \)
then have \( \langle cv,cu\rangle \in r \) using T(2)
then have \( \text{SmallerOf}(r,cu,cv)=cv \) using SmallerOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(5) have \( False \)
have \( x\in X \) using R
ultimately have \( x\in \text{LeftRayX}(X,r,cu) \), \( x\in \text{IntervalX}(X, r, bv, cv) \) using LeftRayX_def, IntervalX_def, Interval_def
then have \( x\in \text{LeftRayX}(X, r, cu) \cap \text{IntervalX}(X, r, bv, cv) \)
then show \( \text{IntervalX}(X, r, bv, \text{SmallerOf}(r, cu, cv)) \subseteq \text{LeftRayX}(X, r, cu) \cap \text{IntervalX}(X, r, bv, cv) \)
qed
The intersection of a left ray and a right ray is an open interval bounded by the two points.
lemma inter_lray_rray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,bu)\cap \text{RightRayX}(X,r,cv)= \text{IntervalX}(X,r,cv,bu) \) unfolding LeftRayX_def, RightRayX_def, IntervalX_def, Interval_defThe intersection of two left rays is the left ray determined by the smaller of the two bounds.
lemma inter_lray_lray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,bu)\cap \text{LeftRayX}(X,r,cv)= \text{LeftRayX}(X,r, \text{SmallerOf}(r,bu,cv)) \)proof{
}
}
fix \( x \)
assume \( x\in \text{LeftRayX}(X,r,bu)\cap \text{LeftRayX}(X,r,cv) \)
then have B: \( x\in X \), \( \langle x,bu\rangle \in r \), \( \langle x,cv\rangle \in r \), \( x\neq bu \), \( x\neq cv \) using LeftRayX_def
then have C: \( \langle x, \text{SmallerOf}(r,bu,cv)\rangle \in r \) using SmallerOf_def
from B have D: \( x\neq \text{SmallerOf}(r,bu,cv) \) using SmallerOf_def
from B, C, D have \( x\in \text{LeftRayX}(X,r, \text{SmallerOf}(r,bu,cv)) \) using LeftRayX_def
then show \( \text{LeftRayX}(X, r, bu) \cap \text{LeftRayX}(X, r, cv) \subseteq \text{LeftRayX}(X, r, \text{SmallerOf}(r, bu, cv)) \)
{
fix \( x \)
assume \( x\in \text{LeftRayX}(X, r, \text{SmallerOf}(r, bu, cv)) \)
then have R: \( x\in X \), \( \langle x, \text{SmallerOf}(r,bu,cv)\rangle \in r \), \( x\neq \text{SmallerOf}(r,bu,cv) \) using LeftRayX_def
{
{
}
}
assume AS: \( \langle bu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,bu,cv)=bu \) using SmallerOf_def
then have A: \( \langle x,bu\rangle \in r \) using R(2)
with AS have \( \langle x,cv\rangle \in r \) using assms(3) unfolding IsLinOrder_def, trans_def
with A have \( \langle x,bu\rangle \in r \), \( \langle x,cv\rangle \in r \)
moreover {
}
ultimately have T: \( \langle x,cv\rangle \in r \), \( \langle x,bu\rangle \in r \)
assume AS: \( \langle bu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,bu,cv)=cv \) using SmallerOf_def
then have xcv: \( \langle x,cv\rangle \in r \) using R(2)
from AS have \( \langle cv,bu\rangle \in r \) using assms, IsLinOrder_def, IsTotal_def, assms
with xcv have \( \langle x,bu\rangle \in r \) using assms(3) unfolding IsLinOrder_def, trans_def
with xcv have \( \langle x,cv\rangle \in r \), \( \langle x,bu\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle x,bu\rangle \in r \), \( \langle x,cv\rangle \in r \), \( x\neq bu \), \( x\neq cv \)
assume AS: \( x=bu \)
then have \( \langle bu,cv\rangle \in r \) using T(1)
then have \( \text{SmallerOf}(r,bu,cv)=bu \) using SmallerOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(3) have \( False \)
assume AS: \( x=cv \)
then have \( \langle cv,bu\rangle \in r \) using T(2)
then have \( \text{SmallerOf}(r,bu,cv)=cv \) using SmallerOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(3) have \( False \)
with R(1) have \( x\in \text{LeftRayX}(X, r, bu) \cap \text{LeftRayX}(X, r, cv) \) using LeftRayX_def
then show \( \text{LeftRayX}(X, r, \text{SmallerOf}(r, bu, cv)) \subseteq \text{LeftRayX}(X, r, bu) \cap \text{LeftRayX}(X, r, cv) \)
qed
The intersection of two right rays is the right ray determined by the greater of the two bounds.
lemma inter_rray_rray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{RightRayX}(X,r,bu)\cap \text{RightRayX}(X,r,cv)= \text{RightRayX}(X,r, \text{GreaterOf}(r,bu,cv)) \)proof{
}
}
fix \( x \)
assume \( x\in \text{RightRayX}(X,r,bu)\cap \text{RightRayX}(X,r,cv) \)
then have B: \( x\in X \), \( \langle bu,x\rangle \in r \), \( \langle cv,x\rangle \in r \), \( x\neq bu \), \( x\neq cv \) using RightRayX_def
then have C: \( \langle \text{GreaterOf}(r,bu,cv),x\rangle \in r \) using GreaterOf_def
from B have D: \( x\neq \text{GreaterOf}(r,bu,cv) \) using GreaterOf_def
from B, C, D have \( x\in \text{RightRayX}(X,r, \text{GreaterOf}(r,bu,cv)) \) using RightRayX_def
then show \( \text{RightRayX}(X, r, bu) \cap \text{RightRayX}(X, r, cv) \subseteq \text{RightRayX}(X, r, \text{GreaterOf}(r, bu, cv)) \)
{
fix \( x \)
assume \( x\in \text{RightRayX}(X, r, \text{GreaterOf}(r, bu, cv)) \)
then have R: \( x\in X \), \( \langle \text{GreaterOf}(r,bu,cv),x\rangle \in r \), \( x\neq \text{GreaterOf}(r,bu,cv) \) using RightRayX_def
{
{
}
}
assume AS: \( \langle bu,cv\rangle \in r \)
then have \( \text{GreaterOf}(r,bu,cv)=cv \) using GreaterOf_def
then have A: \( \langle cv,x\rangle \in r \) using R(2)
with AS have \( \langle bu,x\rangle \in r \) using assms(3) unfolding IsLinOrder_def, trans_def
with A have \( \langle bu,x\rangle \in r \), \( \langle cv,x\rangle \in r \)
moreover {
}
ultimately have T: \( \langle cv,x\rangle \in r \), \( \langle bu,x\rangle \in r \)
assume AS: \( \langle bu,cv\rangle \notin r \)
then have \( \text{GreaterOf}(r,bu,cv)=bu \) using GreaterOf_def
then have bux: \( \langle bu,x\rangle \in r \) using R(2)
from AS have \( \langle cv,bu\rangle \in r \) using assms, IsLinOrder_def, IsTotal_def, assms
with bux have \( \langle cv,x\rangle \in r \) using assms(3) unfolding IsLinOrder_def, trans_def
with bux have \( \langle cv,x\rangle \in r \), \( \langle bu,x\rangle \in r \)
moreover {
}
moreover {
}
ultimately have \( \langle bu,x\rangle \in r \), \( \langle cv,x\rangle \in r \), \( x\neq bu \), \( x\neq cv \)
assume AS: \( x=bu \)
then have \( \langle cv,bu\rangle \in r \) using T(1)
then have \( \text{GreaterOf}(r,bu,cv)=bu \) using GreaterOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(3) have \( False \)
assume AS: \( x=cv \)
then have \( \langle bu,cv\rangle \in r \) using T(2)
then have \( \text{GreaterOf}(r,bu,cv)=cv \) using GreaterOf_def, assms, IsLinOrder_def, antisym_def
with AS, R(3) have \( False \)
with R(1) have \( x\in \text{RightRayX}(X, r, bu) \cap \text{RightRayX}(X, r, cv) \) using RightRayX_def
then show \( \text{RightRayX}(X, r, \text{GreaterOf}(r, bu, cv)) \subseteq \text{RightRayX}(X, r, bu) \cap \text{RightRayX}(X, r, cv) \)
qed
The open intervals and rays satisfy the base condition.
lemma intervals_rays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ satisfies the base condition } \)proof let \( I = \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\} \)
let \( R = \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
let \( L = \{ \text{LeftRayX}(X,r,b).\ b\in X\} \)
let \( B = \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
{
fix \( U \) \( V \)
assume A: \( U\in B \), \( V\in B \)
then have dU: \( U\in I\vee U\in L\vee U\in R \) and dV: \( V\in I\vee V\in L\vee V\in R \)
{
assume S: \( V\in I \)
{
assume \( U\in I \)
with S obtain \( bu \) \( cu \) \( bv \) \( cv \) where A: \( U= \text{IntervalX}(X,r,bu,cu) \), \( V= \text{IntervalX}(X,r,bv,cv) \), \( bu\in X \), \( cu\in X \), \( bv\in X \), \( cv\in X \)
{
assume \( \langle bu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,bu,bv) = bv \) unfolding GreaterOf_def
with A(5) have \( \text{GreaterOf}(r,bu,bv)\in X \)
moreover {
}
ultimately have G: \( \text{GreaterOf}(r,bu,bv)\in X \)
{
assume \( \langle bu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,bu,bv) = bu \) unfolding GreaterOf_def
with A(3) have \( \text{GreaterOf}(r,bu,bv)\in X \)
assume \( \langle cu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,cu,cv) = cu \) unfolding SmallerOf_def
with A(4) have \( \text{SmallerOf}(r,cu,cv)\in X \)
moreover {
}
ultimately have g: \( \text{SmallerOf}(r,cu,cv)\in X \)
assume \( \langle cu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,cu,cv) = cv \) unfolding SmallerOf_def
with A(6) have \( \text{SmallerOf}(r,cu,cv)\in X \)
from G, g, A have \( U\cap V\in B \) using inter_two_intervals, assms
moreover {
}
}
moreover {
}
}
ultimately have \( U\cap V\in B \) using dU
assume \( U\in L \)
with S obtain \( bu \) \( bv \) \( cv \) where A: \( U= \text{LeftRayX}(X, r,bu) \), \( V= \text{IntervalX}(X,r,bv,cv) \), \( bu\in X \), \( bv\in X \), \( cv\in X \)
{
assume \( \langle bu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,bu,cv) = bu \) unfolding SmallerOf_def
with A(3) have \( \text{SmallerOf}(r,bu,cv)\in X \)
moreover {
}
ultimately have g: \( \text{SmallerOf}(r,bu,cv)\in X \)
assume \( \langle bu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,bu,cv) = cv \) unfolding SmallerOf_def
with A(5) have \( \text{SmallerOf}(r,bu,cv)\in X \)
from g, A have \( U\cap V\in B \) using inter_lray_interval, assms
assume \( U\in R \)
with S obtain \( cu \) \( bv \) \( cv \) where A: \( U= \text{RightRayX}(X,r,cu) \), \( V= \text{IntervalX}(X,r,bv,cv) \), \( cu\in X \), \( bv\in X \), \( cv\in X \)
{
assume \( \langle cu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,cu,bv) = bv \) unfolding GreaterOf_def
with A(4) have \( \text{GreaterOf}(r,cu,bv)\in X \)
moreover {
}
ultimately have G: \( \text{GreaterOf}(r,cu,bv)\in X \)
assume \( \langle cu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,cu,bv) = cu \) unfolding GreaterOf_def
with A(3) have \( \text{GreaterOf}(r,cu,bv)\in X \)
with A have \( U\cap V\in B \) using inter_rray_interval, assms
moreover {
}
}
}
moreover {
}
}
}
ultimately have S: \( U\cap V\in B \) using dV
{
assume S: \( V\in L \)
{
assume \( U\in I \)
with S obtain \( bu \) \( bv \) \( cv \) where A: \( V= \text{LeftRayX}(X, r,bu) \), \( U= \text{IntervalX}(X,r,bv,cv) \), \( bu\in X \), \( bv\in X \), \( cv\in X \)
{
assume \( \langle bu,cv\rangle \in r \)
then have \( \text{SmallerOf}(r,bu,cv) = bu \) unfolding SmallerOf_def
with A(3) have \( \text{SmallerOf}(r,bu,cv)\in X \)
moreover {
}
ultimately have g: \( \text{SmallerOf}(r,bu,cv)\in X \)
assume \( \langle bu,cv\rangle \notin r \)
then have \( \text{SmallerOf}(r,bu,cv) = cv \) unfolding SmallerOf_def
with A(5) have \( \text{SmallerOf}(r,bu,cv)\in X \)
have \( U\cap V=V\cap U \)
with A, g have \( U\cap V\in B \) using inter_lray_interval, assms
moreover {
}
moreover {
}
}
ultimately have \( U\cap V\in B \) using dU
assume \( U\in R \)
with S obtain \( bu \) \( cv \) where A: \( V= \text{LeftRayX}(X,r,bu) \), \( U= \text{RightRayX}(X,r,cv) \), \( bu\in X \), \( cv\in X \)
have \( U\cap V=V\cap U \)
with A have \( U\cap V\in B \) using inter_lray_rray, assms
assume \( U\in L \)
with S obtain \( bu \) \( bv \) where A: \( U= \text{LeftRayX}(X,r,bu) \), \( V= \text{LeftRayX}(X,r,bv) \), \( bu\in X \), \( bv\in X \)
{
assume \( \langle bu,bv\rangle \in r \)
then have \( \text{SmallerOf}(r,bu,bv) = bu \) unfolding SmallerOf_def
with A(3) have \( \text{SmallerOf}(r,bu,bv)\in X \)
moreover {
}
ultimately have g: \( \text{SmallerOf}(r,bu,bv)\in X \)
assume \( \langle bu,bv\rangle \notin r \)
then have \( \text{SmallerOf}(r,bu,bv) = bv \) unfolding SmallerOf_def
with A(4) have \( \text{SmallerOf}(r,bu,bv)\in X \)
with A have \( U\cap V\in B \) using inter_lray_lray, assms
assume S: \( V\in R \)
{
assume \( U\in I \)
with S obtain \( cu \) \( bv \) \( cv \) where A: \( V= \text{RightRayX}(X,r,cu) \), \( U= \text{IntervalX}(X,r,bv,cv) \), \( cu\in X \), \( bv\in X \), \( cv\in X \)
{
assume \( \langle cu,bv\rangle \in r \)
then have \( \text{GreaterOf}(r,cu,bv) = bv \) unfolding GreaterOf_def
with A(4) have \( \text{GreaterOf}(r,cu,bv)\in X \)
moreover {
}
ultimately have G: \( \text{GreaterOf}(r,cu,bv)\in X \)
assume \( \langle cu,bv\rangle \notin r \)
then have \( \text{GreaterOf}(r,cu,bv) = cu \) unfolding GreaterOf_def
with A(3) have \( \text{GreaterOf}(r,cu,bv)\in X \)
have \( U\cap V=V\cap U \)
with A, G have \( U\cap V\in B \) using inter_rray_interval, assms
moreover {
}
moreover {
}
}
ultimately have \( U\cap V\in B \) using dU
assume \( U\in L \)
with S obtain \( bu \) \( cv \) where A: \( U= \text{LeftRayX}(X,r,bu) \), \( V= \text{RightRayX}(X,r,cv) \), \( bu\in X \), \( cv\in X \)
then have \( U\cap V\in B \) using inter_lray_rray, assms
assume \( U\in R \)
with S obtain \( cu \) \( cv \) where A: \( U= \text{RightRayX}(X,r,cu) \), \( V= \text{RightRayX}(X,r,cv) \), \( cu\in X \), \( cv\in X \)
{
assume \( \langle cu,cv\rangle \in r \)
then have \( \text{GreaterOf}(r,cu,cv) = cv \) unfolding GreaterOf_def
with A(4) have \( \text{GreaterOf}(r,cu,cv)\in X \)
moreover {
}
ultimately have G: \( \text{GreaterOf}(r,cu,cv)\in X \)
assume \( \langle cu,cv\rangle \notin r \)
then have \( \text{GreaterOf}(r,cu,cv) = cu \) unfolding GreaterOf_def
with A(3) have \( \text{GreaterOf}(r,cu,cv)\in X \)
from G, A have \( U\cap V\in B \) using inter_rray_rray, assms
fix \( x \)
assume \( x\in U\cap V \)
then have \( x\in U\cap V\wedge U\cap V\subseteq U\cap V \)
then have \( \exists W.\ W\in (B)\wedge x\in W \wedge W \subseteq U\cap V \) using S
then have \( \exists W\in (B).\ x\in W \wedge W \subseteq U\cap V \)
hence \( (\forall x \in U\cap V.\ \exists W\in (B).\ x\in W \wedge W \subseteq U\cap V) \)
then show \( thesis \) using SatisfiesBaseCondition_def
qed
Since the intervals and rays form a base of a topology, and this topology is uniquely determined; we can built it. In the definition we have to make sure that we have a totally ordered set.
definition
\( \text{IsLinOrder}(X,r) \Longrightarrow OrdTopology X r \equiv TopologyBase \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
The order topology is indeed a topology, and the collection of open intervals and rays is a base for it.
theorem Ordtopology_is_a_topology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (OrdTopology X r) \text{ is a topology } \) and \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ is a base for } (OrdTopology X r) \) using assms, Base_topology_is_a_topology, intervals_rays_base_condition, OrderTopology_defThe order topology satisfies the assumptions of the topology0 locale.
lemma topology0_ordtopology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( topology0(OrdTopology X r) \) using Ordtopology_is_a_topology, topology0_def, assmsTotal set
The topology is defined in the set \(X\), when \(X\) has more than one point
The union of all open sets in the order topology is all of \(X\), provided \(X\) has at least two distinct points (so that some ray or interval is nonempty).
lemma union_ordtopology:
assumes \( \text{IsLinOrder}(X,r) \), \( \exists x y.\ x\neq y \wedge x\in X\wedge y\in X \)
shows \( \bigcup (OrdTopology X r)=X \)proof let \( B = \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
have base: \( B \text{ is a base for } (OrdTopology X r) \) using Ordtopology_is_a_topology(2), assms(1)
from assms(2) obtain \( x \) \( y \) where T: \( x\neq y \wedge x\in X\wedge y\in X \)
then have B: \( x\in \text{LeftRayX}(X,r,y)\vee x\in \text{RightRayX}(X,r,y) \) using LeftRayX_def, RightRayX_def, assms(1), IsLinOrder_def, IsTotal_def
then have \( x\in \bigcup B \) using T
then have x: \( x\in \bigcup (OrdTopology X r) \) using Top_1_2_L5, base
{
fix \( z \)
assume z: \( z\in X \)
{
assume \( x=z \)
then have \( z\in \bigcup (OrdTopology X r) \) using x
moreover {
}
ultimately have \( z\in \bigcup (OrdTopology X r) \)
assume \( x\neq z \)
with z, T have \( z\in \text{LeftRayX}(X,r,x)\vee z\in \text{RightRayX}(X,r,x) \), \( x\in X \) using LeftRayX_def, RightRayX_def, assms(1), IsLinOrder_def, IsTotal_def
then have \( z\in \bigcup B \)
then have \( z\in \bigcup (OrdTopology X r) \) using Top_1_2_L5, base
then show \( X\subseteq \bigcup (OrdTopology X r) \)
have \( \bigcup B\subseteq X \) using IntervalX_def, LeftRayX_def, RightRayX_def
then show \( \bigcup (OrdTopology X r)\subseteq X \) using Top_1_2_L5, base
qed
Right order and Left order topologies.
Notice that the left and right rays are closed under intersection, hence they form a base of a topology. They are called right order topology and left order topology respectively.
If the order in \(X\) has a minimal or a maximal element, is necessary to consider \(X\) as an element of the base or that limit point wouldn't be in any basic open set.
lemma leftrays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ satisfies the base condition } \)proof{
}
fix \( U \) \( V \)
assume \( U\in \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \), \( V\in \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
then obtain \( b \) \( c \) where A: \( (b\in X\wedge U= \text{LeftRayX}(X,r,b))\vee U=X \), \( (c\in X\wedge V= \text{LeftRayX}(X,r,c))\vee V=X \), \( U\subseteq X \), \( V\subseteq X \) unfolding LeftRayX_def
then have \( (U\cap V= \text{LeftRayX}(X,r, \text{SmallerOf}(r,b,c))\wedge b\in X\wedge c\in X)\vee U\cap V=X\vee (U\cap V= \text{LeftRayX}(X,r,c)\wedge c\in X)\vee (U\cap V= \text{LeftRayX}(X,r,b)\wedge b\in X) \) using inter_lray_lray, assms
moreover
have \( b\in X\wedge c\in X \longrightarrow \text{SmallerOf}(r,b,c)\in X \) unfolding SmallerOf_def
ultimately have \( U\cap V\in \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
hence \( \forall x\in U\cap V.\ \exists W\in \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\}.\ x\in W\wedge W\subseteq U\cap V \)
then show \( thesis \) using SatisfiesBaseCondition_def
qed
The collection of right open rays together with the whole space satisfies the base condition.
lemma rightrays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ satisfies the base condition } \)proof{
}
fix \( U \) \( V \)
assume \( U\in \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \), \( V\in \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
then obtain \( b \) \( c \) where A: \( (b\in X\wedge U= \text{RightRayX}(X,r,b))\vee U=X \), \( (c\in X\wedge V= \text{RightRayX}(X,r,c))\vee V=X \), \( U\subseteq X \), \( V\subseteq X \) unfolding RightRayX_def
then have \( (U\cap V= \text{RightRayX}(X,r, \text{GreaterOf}(r,b,c))\wedge b\in X\wedge c\in X)\vee U\cap V=X\vee (U\cap V= \text{RightRayX}(X,r,c)\wedge c\in X)\vee (U\cap V= \text{RightRayX}(X,r,b)\wedge b\in X) \) using inter_rray_rray, assms
moreover
have \( b\in X\wedge c\in X \longrightarrow \text{GreaterOf}(r,b,c)\in X \) using GreaterOf_def
ultimately have \( U\cap V\in \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
hence \( \forall x\in U\cap V.\ \exists W\in \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\}.\ x\in W\wedge W\subseteq U\cap V \)
then show \( thesis \) using SatisfiesBaseCondition_def
qed
The left order topology is the topology generated by the collection of left open rays together with the whole space.
definition
\( \text{IsLinOrder}(X,r) \Longrightarrow LOrdTopology X r \equiv TopologyBase \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
The right order topology is the topology generated by the collection of right open rays together with the whole space.
definition
\( \text{IsLinOrder}(X,r) \Longrightarrow ROrdTopology X r \equiv TopologyBase \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
The left and right order topologies are topologies, with the respective ray families (together with the whole space) as bases.
theorem LOrdtopology_ROrdtopology_are_topologies:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (LOrdTopology X r) \text{ is a topology } \) and \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (LOrdTopology X r) \) and \( (ROrdTopology X r) \text{ is a topology } \) and \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (ROrdTopology X r) \) using Base_topology_is_a_topology, leftrays_base_condition, assms, rightrays_base_condition, LeftOrderTopology_def, RightOrderTopology_defBoth the left and the right order topologies satisfy the assumptions of the topology0 locale.
lemma topology0_lordtopology_rordtopology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( topology0(LOrdTopology X r) \) and \( topology0(ROrdTopology X r) \) using LOrdtopology_ROrdtopology_are_topologies, topology0_def, assmsThe topology is defined on the set \(X\)
lemma union_lordtopology_rordtopology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \bigcup (LOrdTopology X r)=X \) and \( \bigcup (ROrdTopology X r)=X \)proof have baseL: \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (LOrdTopology X r) \) using LOrdtopology_ROrdtopology_are_topologies(2), assms
have baseR: \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (ROrdTopology X r) \) using LOrdtopology_ROrdtopology_are_topologies(4), assms
show \( \bigcup (LOrdTopology X r)=X \) using Top_1_2_L5, baseL unfolding LeftRayX_def
show \( \bigcup (ROrdTopology X r)=X \) using Top_1_2_L5, baseR unfolding RightRayX_def
qed
Union of Topologies
The union of two topologies is not a topology. A way to overcome this fact is to define the following topology:
Given a family of topologies on the same underlying set, the join topology is defined as the unique topology for which the union of all members is a subbase.
definition
\( (\forall T\in M.\ T\text{ is a topology } \wedge (\forall Q\in M.\ \bigcup Q=\bigcup T)) \Longrightarrow (joinT M \equiv \text{The } T.\ (\bigcup M)\text{ is a subbase for } T) \)
The first result states that from any family of sets we get a base using finite intersections of them. The second one states that any family of sets is a subbase of some topology.
theorem subset_as_subbase:
shows \( \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ satisfies the base condition } \)proof{
}
}
fix \( U \) \( V \)
assume A: \( U\in \{\bigcap A.\ A \in \text{FinPow}(B)\} \wedge V\in \{\bigcap A.\ A \in \text{FinPow}(B)\} \)
then obtain \( M \) \( R \) where MR: \( Finite(M) \), \( Finite(R) \), \( M\subseteq B \), \( R\subseteq B \), \( U=\bigcap M \), \( V=\bigcap R \) using FinPow_def
{
fix \( x \)
assume AS: \( x\in U\cap V \)
then have N: \( M\neq 0 \), \( R\neq 0 \) using MR(5,6)
have \( Finite(M \cup R) \) using MR(1,2)
moreover
have \( M \cup R\in Pow(B) \) using MR(3,4)
ultimately have \( M\cup R\in \text{FinPow}(B) \) using FinPow_def
then have \( \bigcap (M\cup R)\in \{\bigcap A.\ A \in \text{FinPow}(B)\} \)
moreover
}
from N have \( \bigcap (M\cup R)\subseteq \bigcap M \), \( \bigcap (M\cup R)\subseteq \bigcap R \)
then have \( \bigcap (M\cup R)\subseteq U\cap V \) using MR(5,6)
moreover {
fix \( S \)
assume \( S\in M \cup R \)
then have \( S\in M\vee S\in R \)
then have \( x\in S \) using AS, MR(5,6)
then have \( x\in \bigcap (M \cup R) \) using N
ultimately have \( \exists W\in \{\bigcap A.\ A \in \text{FinPow}(B)\}.\ x\in W\wedge W\subseteq U\cap V \)
then have \( (\forall x \in U\cap V.\ \exists W\in \{\bigcap A.\ A \in \text{FinPow}(B)\}.\ x\in W \wedge W \subseteq U\cap V) \)
then have \( \forall U V.\ ((U\in \{\bigcap A.\ A \in \text{FinPow}(B)\} \wedge V\in \{\bigcap A.\ A \in \text{FinPow}(B)\}) \longrightarrow \)
\( (\forall x \in U\cap V.\ \exists W\in \{\bigcap A.\ A \in \text{FinPow}(B)\}.\ x\in W \wedge W \subseteq U\cap V)) \)
then show \( \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ satisfies the base condition } \) using SatisfiesBaseCondition_def
qed
Any family of sets is a subbase for a topology: the topology of all unions of finite intersections of members of the family.
theorem Top_subbase:
assumes \( T = \{\bigcup A.\ A\in Pow(\{\bigcap A.\ A \in \text{FinPow}(B)\})\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a subbase for } T \)proof{
}
fix \( S \)
assume \( S\in B \)
then have \( \{S\}\in \text{FinPow}(B) \), \( \bigcap \{S\}=S \) using FinPow_def
then have \( \{S\}\in Pow(\{\bigcap A.\ A \in \text{FinPow}(B)\}) \)
then have \( \bigcup \{S\}\in \{\bigcup A.\ A\in Pow(\{\bigcap A.\ A \in \text{FinPow}(B)\})\} \)
then have \( S\in \{\bigcup A.\ A\in Pow(\{\bigcap A.\ A \in \text{FinPow}(B)\})\} \)
then have \( S\in T \) using assms
then have \( B\subseteq T \)
moreover
qed
have \( \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ satisfies the base condition } \) using subset_as_subbase
then have \( T \text{ is a topology } \) and \( \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ is a base for } T \) using Top_1_2_T1, assms
ultimately show \( T \text{ is a topology } \) and \( B\text{ is a subbase for }T \) using IsAsubBaseFor_def
A subbase defines a unique topology.
theorem same_subbase_same_top:
assumes \( B \text{ is a subbase for } T \) and \( B \text{ is a subbase for } S \)
shows \( T = S \) using IsAsubBaseFor_def, assms, same_base_same_top end
theorem Top_1_2_T1:
assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \) lemma same_base_same_top:
assumes \( B \text{ is a base for } T \) and \( B \text{ is a base for } S \)
shows \( T = S \)Definition of TopologyWithBase:
\( U \text{ satisfies the base condition } \Longrightarrow TopologyBase U \equiv \text{The } T.\ U \text{ is a base for } T \)
theorem Top_1_2_T1:
assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \)Definition of IsAbaseFor:
\( B \text{ is a base for } T \equiv B\subseteq T \wedge T = \{\bigcup A.\ A\in Pow(B)\} \)
lemma (in topology0) Top_2_L5:
assumes \( U\subseteq A \) and \( U\in T \)
shows \( U \subseteq int(A) \) lemma point_open_base_neigh:
assumes \( B \text{ is a base for } T \) and \( U\in T \) and \( x\in U \)
shows \( \exists V\in B.\ V\subseteq U \wedge x\in V \) lemma (in topology0) Top_2_L2: shows \( int(A) \in T \)
lemma (in topology0) Top_2_L1: shows \( int(A) \subseteq A \)
lemma (in topology0) Top_3_L11:
assumes \( A \subseteq \bigcup T \)
shows \( cl(A) \subseteq \bigcup T \), \( cl(\bigcup T \setminus A) = \bigcup T \setminus int(A) \) lemma base_sets_open:
assumes \( B \text{ is a base for } T \) and \( U \in B \)
shows \( U \in T \) lemma (in topology0) cl_inter_neigh:
assumes \( A \subseteq \bigcup T \) and \( U\in T \) and \( x \in cl(A) \cap U \)
shows \( A\cap U \neq 0 \) lemma (in topology0) inter_neigh_cl:
assumes \( A \subseteq \bigcup T \) and \( x\in \bigcup T \) and \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)
shows \( x \in cl(A) \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge (\bigcup T)\setminus D \in T) \)
Definition of DualBase:
\( B\text{ is a base for }T \Longrightarrow DualBase B T\equiv \{\bigcup T-U.\ U\in B\}\cup \{\bigcup T\} \)
lemma (in topology0) Top_3_L1: shows \( (\bigcup T) \text{ is closed in } T \)
lemma (in topology0) Top_3_L9:
assumes \( A\in T \)
shows \( (\bigcup T - A) \text{ is closed in } T \)Definition of Closure:
\( \text{Closure}(A,T) \equiv \bigcap Closed \text{Covers}(A,T) \)
Definition of ClosedCovers:
\( Closed \text{Covers}(A,T) \equiv \{D \in Pow(\bigcup T).\ D \text{ is closed in } T \wedge A\subseteq D\} \)
lemma closure_set_base_topology:
assumes \( U \text{ is a base for } Q \), \( Q\text{ is a topology } \), \( A\subseteq \bigcup Q \)
shows \( \text{Closure}(A,Q) = \{x\in \bigcup Q.\ \forall T\in U.\ x\in T\longrightarrow A\cap T\neq 0\} \)Definition of IsAPartition:
\( (U \text{ is a partition of } X) \equiv (\bigcup U=X \wedge (\forall A\in U.\ \forall B\in U.\ A=B\vee A\cap B=0)\wedge 0\notin U) \)
Definition of SatisfiesBaseCondition:
\( B \text{ satisfies the base condition } \equiv \)
\( \forall U V.\ ((U\in B \wedge V\in B) \longrightarrow (\forall x \in U\cap V.\ \exists W\in B.\ x\in W \wedge W \subseteq U\cap V)) \)
theorem Base_topology_is_a_topology:
assumes \( U \text{ satisfies the base condition } \)
shows \( (TopologyBase U) \text{ is a topology } \) and \( U \text{ is a base for } (TopologyBase U) \) lemma partition_base_condition:
assumes \( P \text{ is a partition of } X \)
shows \( P \text{ satisfies the base condition } \)Definition of PartitionTopology:
\( (U \text{ is a partition of } X) \Longrightarrow PTopology X U \equiv TopologyBase U \)
theorem Ptopology_is_a_topology:
assumes \( U \text{ is a partition of } X \)
shows \( (PTopology X U) \text{ is a topology } \) and \( U \text{ is a base for } (PTopology X U) \) theorem Ptopology_is_a_topology:
assumes \( U \text{ is a partition of } X \)
shows \( (PTopology X U) \text{ is a topology } \) and \( U \text{ is a base for } (PTopology X U) \) lemma Top_1_2_L5:
assumes \( B \text{ is a base for } T \)
shows \( \bigcup T = \bigcup B \) lemma union_ptopology:
assumes \( U \text{ is a partition of } X \)
shows \( \bigcup (PTopology X U)=X \) lemma Top_1_2_L1:
assumes \( B \text{ is a base for } T \) and \( U\in T \)
shows \( \exists A\in Pow(B).\ U = \bigcup A \) lemma diff_union_is_union_diff:
assumes \( R\subseteq P \), \( P \text{ is a partition of } X \)
shows \( X - \bigcup R=\bigcup (P-R) \) lemma (in topology0) open_open_neigh:
assumes \( V\in T \)
shows \( \forall x\in V.\ \exists U\in T.\ (x\in U \wedge U\subseteq V) \) lemma topology0_ptopology:
assumes \( U \text{ is a partition of } X \)
shows \( topology0(PTopology X U) \) lemma (in topology0) Top_3_L4:
assumes \( K\neq 0 \) and \( \forall D\in K.\ D \text{ is closed in } T \)
shows \( (\bigcap K) \text{ is closed in } T \) lemma closed_sets_ptopology:
assumes \( T \text{ is a partition of } X \)
shows \( D \text{ is closed in } (PTopology X T) \longleftrightarrow D\in (PTopology X T) \) lemma (in topology0) Top_2_L6:
assumes \( \exists U\in T.\ (x\in U \wedge U\subseteq A) \)
shows \( x \in int(A) \) lemma closure_set_ptopology:
assumes \( U \text{ is a partition of } X \), \( A\subseteq X \)
shows \( \text{Closure}(A,(PTopology X U))=\bigcup \{T\in U.\ T\cap A\neq 0\} \) lemma interior_set_base_topology:
assumes \( U \text{ is a base for } T \), \( T\text{ is a topology } \)
shows \( \text{Interior}(A,T) = \bigcup \{T\in U.\ T\subseteq A\} \) lemma (in topology0) Top_3_L12:
assumes \( A \subseteq \bigcup T \)
shows \( \partial A = cl(A) - int(A) \) lemma subpartition:
assumes \( U \text{ is a partition of } X \), \( V\subseteq U \)
shows \( V\text{ is a partition of }\bigcup V \) lemma discrete_partition: shows \( \{\{x\}.\ x\in X\} \text{ is a partition of }X \)
lemma indiscrete_partition:
assumes \( X\neq 0 \)
shows \( \{X\} \text{ is a partition of } X \) theorem Ptopology_is_a_topology:
assumes \( U \text{ is a partition of } X \)
shows \( (PTopology X U) \text{ is a topology } \) and \( U \text{ is a base for } (PTopology X U) \) lemma empty_open:
assumes \( T \text{ is a topology } \)
shows \( \emptyset \in T \) lemma union_open:
assumes \( T \text{ is a topology } \) and \( \forall A\in \mathcal{A} .\ A \in T \)
shows \( (\bigcup \mathcal{A} ) \in T \) lemma subspace_base_topology:
assumes \( B \text{ is a base for } T \)
shows \( (B \text{ restricted to } Y) \text{ is a base for } (T \text{ restricted to } Y) \) lemma base_no_0: shows \( B\text{ is a base for }T \longleftrightarrow (B-\{0\})\text{ is a base for }T \)
lemma restriction_partition:
assumes \( U \text{ is a partition of }X \)
shows \( ((U \text{ restricted to } Y)-\{0\}) \text{ is a partition of } (X\cap Y) \)Definition of IntervalX:
\( \text{IntervalX}(X,r,b,c)\equiv ( \text{Interval}(r,b,c)\cap X)-\{b,c\} \)
lemma Order_ZF_2_L1A:
assumes \( x \in \text{Interval}(r,a,b) \)
shows \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \)Definition of GreaterOf:
\( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
Definition of SmallerOf:
\( \text{SmallerOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }a\text{ else }b) \)
lemma Order_ZF_2_L1: shows \( x \in \text{Interval}(r,a,b) \longleftrightarrow \langle a,x\rangle \in r \wedge \langle x,b\rangle \in r \)
Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of RightRayX:
\( \text{RightRayX}(X,r,b)\equiv \{c\in X.\ \langle b,c\rangle \in r\}-\{b\} \)
Definition of LeftRayX:
\( \text{LeftRayX}(X,r,b)\equiv \{c\in X.\ \langle c,b\rangle \in r\}-\{b\} \)
Definition of Interval:
\( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
lemma inter_two_intervals:
assumes \( bu\in X \), \( bv\in X \), \( cu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{IntervalX}(X,r,bu,cu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv), \text{SmallerOf}(r,cu,cv)) \) lemma inter_lray_interval:
assumes \( bv\in X \), \( cu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,cu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r,bv, \text{SmallerOf}(r,cu,cv)) \) lemma inter_rray_interval:
assumes \( bv\in X \), \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{RightRayX}(X,r,bu)\cap \text{IntervalX}(X,r,bv,cv)= \text{IntervalX}(X,r, \text{GreaterOf}(r,bu,bv),cv) \) lemma inter_lray_rray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,bu)\cap \text{RightRayX}(X,r,cv)= \text{IntervalX}(X,r,cv,bu) \) lemma inter_lray_lray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{LeftRayX}(X,r,bu)\cap \text{LeftRayX}(X,r,cv)= \text{LeftRayX}(X,r, \text{SmallerOf}(r,bu,cv)) \) lemma inter_rray_rray:
assumes \( bu\in X \), \( cv\in X \), \( \text{IsLinOrder}(X,r) \)
shows \( \text{RightRayX}(X,r,bu)\cap \text{RightRayX}(X,r,cv)= \text{RightRayX}(X,r, \text{GreaterOf}(r,bu,cv)) \) lemma intervals_rays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ satisfies the base condition } \)Definition of OrderTopology:
\( \text{IsLinOrder}(X,r) \Longrightarrow OrdTopology X r \equiv TopologyBase \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \)
theorem Ordtopology_is_a_topology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (OrdTopology X r) \text{ is a topology } \) and \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ is a base for } (OrdTopology X r) \) theorem Ordtopology_is_a_topology:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (OrdTopology X r) \text{ is a topology } \) and \( \{ \text{IntervalX}(X,r,b,c).\ \langle b,c\rangle \in X\times X\}\cup \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{ \text{RightRayX}(X,r,b).\ b\in X\} \text{ is a base for } (OrdTopology X r) \) lemma leftrays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ satisfies the base condition } \) lemma rightrays_base_condition:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ satisfies the base condition } \)Definition of LeftOrderTopology:
\( \text{IsLinOrder}(X,r) \Longrightarrow LOrdTopology X r \equiv TopologyBase \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
Definition of RightOrderTopology:
\( \text{IsLinOrder}(X,r) \Longrightarrow ROrdTopology X r \equiv TopologyBase \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \)
theorem LOrdtopology_ROrdtopology_are_topologies:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (LOrdTopology X r) \text{ is a topology } \) and \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (LOrdTopology X r) \) and \( (ROrdTopology X r) \text{ is a topology } \) and \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (ROrdTopology X r) \) theorem LOrdtopology_ROrdtopology_are_topologies:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (LOrdTopology X r) \text{ is a topology } \) and \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (LOrdTopology X r) \) and \( (ROrdTopology X r) \text{ is a topology } \) and \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (ROrdTopology X r) \) theorem LOrdtopology_ROrdtopology_are_topologies:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( (LOrdTopology X r) \text{ is a topology } \) and \( \{ \text{LeftRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (LOrdTopology X r) \) and \( (ROrdTopology X r) \text{ is a topology } \) and \( \{ \text{RightRayX}(X,r,b).\ b\in X\}\cup \{X\} \text{ is a base for } (ROrdTopology X r) \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
theorem subset_as_subbase: shows \( \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ satisfies the base condition } \)
theorem Top_1_2_T1:
assumes \( B \text{ satisfies the base condition } \) and \( T = \{\bigcup A.\ A\in Pow(B)\} \)
shows \( T \text{ is a topology } \) and \( B \text{ is a base for } T \)Definition of IsAsubBaseFor:
\( B \text{ is a subbase for } T \equiv \)
\( B \subseteq T \wedge \{\bigcap A.\ A \in \text{FinPow}(B)\} \text{ is a base for } T \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
