IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Real_ZF_2 imports OrderedField_ZF MetricSpace_ZF
begin

Isabelle/ZF and IsarMathLib do not have a set of real numbers built-in. The Real_ZF and Real_ZF_1 theories provide a construction but here we do not use it in any way and we just assume that we have a model of real numbers (i.e. a completely ordered field) as defined in the Ordered_Field theory. The construction only assures us that objects with the desired properties exist in the ZF world.

Basic notation for real numbers

In this section we define notation that we will use whenever real numbers play a role, i.e. most of mathematics.

The next locale sets up notation for contexts where real numbers are used.

Locale reals

assumes R_are_reals: \( \text{IsAmodelOfReals}(\mathbb{R} ,Add,Mul, ROrd) \)

defines \( 0 \equiv \text{ TheNeutralElement}(\mathbb{R} ,Add) \)

defines \( 1 \equiv \text{ TheNeutralElement}(\mathbb{R} ,Mul) \)

defines \( x \cdot y \equiv Mul\langle x,y\rangle \)

defines \( x + y \equiv Add\langle x,y\rangle \)

defines \( ( - x) \equiv \text{GroupInv}(\mathbb{R} ,Add)(x) \)

defines \( x - y \equiv x + ( - y) \)

defines \( x \leq y \equiv \langle x,y\rangle \in ROrd \)

defines \( x \lt y \equiv x\leq y \wedge x\neq y \)

defines \( \mathbb{R} ^+ \equiv \text{Nonnegative}(\mathbb{R} ,Add, ROrd) \)

defines \( \mathbb{R} _+ \equiv \text{PositiveSet}(\mathbb{R} ,Add, ROrd) \)

defines \( -A \equiv \text{GroupInv}(\mathbb{R} ,Add)(A) \)

defines \( \mathbb{R} _0 \equiv \mathbb{R} -\{ 0 \} \)

defines \( \vert x\vert \equiv \text{AbsoluteValue}(\mathbb{R} ,Add,ROrd)(x) \)

defines \( dist \equiv \{\langle p,\vert \text{fst}(p) - \text{snd}(p)\vert \rangle .\ p \in \mathbb{R} \times \mathbb{R} \} \)

defines \( 2 \equiv 1 + 1 \)

defines \( x^{-1} \equiv \text{GroupInv}(\mathbb{R} _0,\text{restrict}(Mul,\mathbb{R} _0\times \mathbb{R} _0))(x) \)

defines \( x^2 \equiv x\cdot x \)

defines \( f^\circ \equiv \text{OddExtension}(\mathbb{R} ,Add,ROrd,f) \)

defines \( disk(c,r) \equiv \text{Disk}(\mathbb{R} ,dist,ROrd,c,r) \)

The assumtions of the field1 locale (that sets the context for ordered fields) hold in the reals locale

lemma (in reals) field1_is_valid:

shows \( field1(\mathbb{R} , Add, Mul,ROrd) \)proof
from R_are_reals show \( \text{IsAring}(\mathbb{R} , Add, Mul) \) and \( Mul \text{ is commutative on } \mathbb{R} \) and \( ROrd \subseteq \mathbb{R} \times \mathbb{R} \) and \( \text{IsLinOrder}(\mathbb{R} , ROrd) \) and \( \forall x y.\ \forall z\in \mathbb{R} .\ \langle x, y\rangle \in ROrd \longrightarrow \langle Add\langle x, z\rangle , Add\langle y, z\rangle \rangle \in ROrd \) and \( \text{Nonnegative}(\mathbb{R} , Add, ROrd) \text{ is closed under } Mul \) and \( \text{ TheNeutralElement}(\mathbb{R} , Add) \neq \text{ TheNeutralElement}(\mathbb{R} , Mul) \) and \( \forall x\in \mathbb{R} .\ x \neq \text{ TheNeutralElement}(\mathbb{R} ,Add) \longrightarrow (\exists y\in \mathbb{R} .\ Mul\langle x, y\rangle = \text{ TheNeutralElement}(\mathbb{R} ,Mul)) \) using IsAmodelOfReals_def , IsAnOrdField_def , IsAnOrdRing_def
qed

We can use theorems proven in the field1 locale in the reals locale. Note that since the the field1 locale is an extension of the ring1 locale, which is an extension of ring0 locale , this makes available also the theorems proven in the ring1 and ring0 locales.

Sublocale reals < field1

using field1_is_valid

The group3 locale from the OrderedGroup_ZF theory defines context for theorems about ordered groups. We can use theorems proven in there in the reals locale as real numbers with addition form an ordered group.

Sublocale reals < group3

unfolding group3_def using OrdRing_ZF_1_L4

Since real numbers with addition form a group we can use the theorems proven in the group0 locale defined in the Group_ZF theory in the reals locale.

Sublocale reals < group0

unfolding group3_def using OrderedGroup_ZF_1_L1

Let's recall basic properties of the real line.

lemma (in reals) basic_props:

shows \( ROrd \text{ is total on } \mathbb{R} \) and \( Add \text{ is commutative on } \mathbb{R} \) using OrdRing_ZF_1_L4(2,3)

The distance function dist defined in the reals locale is a metric.

lemma (in reals) dist_is_metric:

shows \( dist : \mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R} ^+ \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = \vert x - y\vert \), \( \forall x\in \mathbb{R} .\ dist\langle x,x\rangle = 0 \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = dist\langle y,x\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ \vert x - z\vert \leq \vert x - y\vert + \vert y - z\vert \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ dist\langle x,z\rangle \leq dist\langle x, y\rangle + dist\langle y,z\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = 0 \longrightarrow x=y \), \( \text{IsApseudoMetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \), \( \text{IsAmetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \)proof
show I: \( dist : \mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R} ^+ \) using group_op_closed , inverse_in_group , OrdRing_ZF_1_L4 , OrderedGroup_ZF_3_L3B , ZF_fun_from_total
then show II: \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = \vert x - y\vert \) using ZF_fun_from_tot_val0
then show III: \( \forall x\in \mathbb{R} .\ dist\langle x,x\rangle = 0 \) using group0_2_L6 , OrderedGroup_ZF_3_L2A
{
fix \( x \) \( y \)
assume \( x\in \mathbb{R} \), \( y\in \mathbb{R} \)
then have \( ( - (x - y)) = y - x \) using group0_2_L12
moreover
from \( x\in \mathbb{R} \), \( y\in \mathbb{R} \) have \( \vert - (x - y)\vert =\vert x - y\vert \) using group_op_closed , inverse_in_group , basic_props(1) , OrderedGroup_ZF_3_L7A
ultimately have \( \vert y - x\vert = \vert x - y\vert \)
with \( x\in \mathbb{R} \), \( y\in \mathbb{R} \), II have \( dist\langle x,y\rangle = dist\langle y,x\rangle \)
}
thus IV: \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = dist\langle y,x\rangle \)
{
fix \( x \) \( y \)
assume \( x\in \mathbb{R} \), \( y\in \mathbb{R} \), \( dist\langle x,y\rangle = 0 \)
with II have \( \vert x - y\vert = 0 \)
with \( x\in \mathbb{R} \), \( y\in \mathbb{R} \) have \( x - y = 0 \) using group_op_closed , inverse_in_group , OrderedGroup_ZF_3_L3D
with \( x\in \mathbb{R} \), \( y\in \mathbb{R} \) have \( x=y \) using group0_2_L11A
}
thus V: \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = 0 \longrightarrow x=y \)
{
fix \( x \) \( y \) \( z \)
assume \( x\in \mathbb{R} \), \( y\in \mathbb{R} \), \( z\in \mathbb{R} \)
then have \( \vert x - z\vert = \vert (x - y) + (y - z)\vert \) using cancel_middle(5)
with \( x\in \mathbb{R} \), \( y\in \mathbb{R} \), \( z\in \mathbb{R} \) have \( \vert x - z\vert \leq \vert x - y\vert + \vert y - z\vert \) using group_op_closed , inverse_in_group , OrdRing_ZF_1_L4(2,3) , OrdGroup_triangle_ineq
}
thus \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ \vert x - z\vert \leq \vert x - y\vert + \vert y - z\vert \)
with II show \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ dist\langle x,z\rangle \leq dist\langle x, y\rangle + dist\langle y,z\rangle \)
with I, III, IV, V show \( \text{IsApseudoMetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \) and \( \text{IsAmetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \) unfolding IsApseudoMetric_def , IsAmetric_def
qed

Real numbers form an ordered loop.

lemma (in reals) reals_loop:

shows \( \text{IsAnOrdLoop}(\mathbb{R} ,Add,ROrd) \)proof
have \( \text{IsAloop}(\mathbb{R} ,Add) \) using group_is_loop
moreover
from R_are_reals have \( ROrd \subseteq \mathbb{R} \times \mathbb{R} \) and \( \text{IsPartOrder}(\mathbb{R} ,ROrd) \) using IsAmodelOfReals_def , IsAnOrdField_def , IsAnOrdRing_def , Order_ZF_1_L2
moreover {
fix \( x \) \( y \) \( z \)
assume A: \( x\in \mathbb{R} \), \( y\in \mathbb{R} \), \( z\in \mathbb{R} \)
then have \( x\leq y \longleftrightarrow x + z \leq y + z \) using ord_transl_inv , ineq_cancel_right
moreover
from A have \( x\leq y \longleftrightarrow z + x \leq z + y \) using ord_transl_inv , OrderedGroup_ZF_1_L5AE
ultimately have \( (x\leq y \longleftrightarrow x + z \leq y + z) \wedge (x\leq y \longleftrightarrow z + x \leq z + y) \)
} ultimately show \( \text{IsAnOrdLoop}(\mathbb{R} ,Add,ROrd) \) unfolding IsAnOrdLoop_def
qed

The assumptions of the pmetric_space locale hold in the reals locale.

lemma (in reals) pmetric_space_valid:

shows \( pmetric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \) unfolding pmetric_space_def , pmetric_space_axioms_def , loop1_def using reals_loop , dist_is_metric(8)

Some properties of the order relation on reals:

lemma (in reals) pos_is_lattice:

shows \( \text{IsLinOrder}(\mathbb{R} ,ROrd) \), \( \text{IsLinOrder}(\mathbb{R} _+,ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \), \( (ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \text{ is a lattice on } \mathbb{R} _+ \)proof
show \( \text{IsLinOrder}(\mathbb{R} ,ROrd) \) using OrdRing_ZF_1_L1 unfolding IsAnOrdRing_def
moreover
have \( \mathbb{R} _+ \subseteq \mathbb{R} \) using pos_set_in_gr
ultimately show \( \text{IsLinOrder}(\mathbb{R} _+,ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \) using ord_linear_subset(2)
moreover
have \( (ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \subseteq \mathbb{R} _+\times \mathbb{R} _+ \)
ultimately show \( (ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \text{ is a lattice on } \mathbb{R} _+ \) using lin_is_latt
qed

We define the topology on reals as one consisting of the unions of open disks.

Definition (in reals)

\( \tau _\mathbb{R} \equiv \{\bigcup A.\ A \in Pow(\bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\})\} \)

Real numbers form a topological space with topology generated by open disks.

theorem (in reals) reals_is_top:

shows \( \tau _\mathbb{R} \text{ is a topology } \) and \( \bigcup \tau _\mathbb{R} = \mathbb{R} \)proof
let \( B = \bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\} \)
have \( pmetric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \) using pmetric_space_valid
moreover
have \( \text{IsMeetSemilattice}(\mathbb{R} _+,ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \) using pos_is_lattice(3) unfolding IsAlattice_def
moreover
from R_are_reals have \( \mathbb{R} _+\neq 0 \) unfolding IsAmodelOfReals_def , IsAnOrdField_def using ordring_one_is_pos
moreover
have \( B = (\bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\}) \)
moreover
have \( \tau _\mathbb{R} = \{\bigcup A.\ A \in Pow(B)\} \) unfolding RealTopology_def
ultimately show \( \tau _\mathbb{R} \text{ is a topology } \) and \( \bigcup \tau _\mathbb{R} = \mathbb{R} \) using pmetric_is_top
qed
end
Definition of IsAmodelOfReals: \( \text{IsAmodelOfReals}(K,A,M,r) \equiv \text{IsAnOrdField}(K,A,M,r) \wedge (r \text{ is complete }) \)
Definition of IsAnOrdField: \( \text{IsAnOrdField}(K,A,M,r) \equiv ( \text{IsAnOrdRing}(K,A,M,r) \wedge \) \( (M \text{ is commutative on } K) \wedge \) \( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \) \( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \) \( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
Definition of IsAnOrdRing: \( \text{IsAnOrdRing}(R,A,M,r) \equiv \) \( ( \text{IsAring}(R,A,M) \wedge (M \text{ is commutative on } R) \wedge \) \( r\subseteq R\times R \wedge \text{IsLinOrder}(R,r) \wedge \) \( (\forall a b.\ \forall c\in R.\ \langle a,b\rangle \in r \longrightarrow \langle A\langle a,c\rangle ,A\langle b,c\rangle \rangle \in r) \wedge \) \( ( \text{Nonnegative}(R,A,r) \text{ is closed under } M)) \)
lemma (in ring1) OrdRing_ZF_1_L4: shows \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \), \( group3(R,A,r) \)
lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in ring1) OrdRing_ZF_1_L4: shows \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \), \( group3(R,A,r) \)
lemma (in group3) OrderedGroup_ZF_3_L3B:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( |a| \in G^+ \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
lemma ZF_fun_from_tot_val0:

assumes \( f:X\rightarrow Y \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( \forall x\in X.\ f(x) = b(x) \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
lemma (in group3) OrderedGroup_ZF_3_L2A: shows \( |1 | = 1 \)
lemma (in group0) group0_2_L12:

assumes \( a\in G \), \( b\in G \)

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)
lemma (in reals) basic_props: shows \( ROrd \text{ is total on } \mathbb{R} \) and \( Add \text{ is commutative on } \mathbb{R} \)
lemma (in group3) OrderedGroup_ZF_3_L7A:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( |a^{-1}| = |a| \)
lemma (in group3) OrderedGroup_ZF_3_L3D:

assumes \( a\in G \) and \( |a| = 1 \)

shows \( a = 1 \)
lemma (in group0) group0_2_L11A:

assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} = 1 \)

shows \( a=b \)
lemma (in group0) cancel_middle:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot c \), \( (a\cdot b)\cdot (c\cdot b)^{-1} = a\cdot c^{-1} \), \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = b \), \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b \), \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \)
theorem (in group3) OrdGroup_triangle_ineq:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \)

shows \( |a\cdot b| \leq |a|\cdot |b| \)
Definition of IsApseudoMetric: \( \text{IsApseudoMetric}(d,X,G,A,r) \equiv d:X\times X \rightarrow \text{Nonnegative}(G,A,r) \) \( \wedge (\forall x\in X.\ d\langle x,x\rangle = \text{ TheNeutralElement}(G,A))\) \( \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = d\langle y,x\rangle )\) \( \wedge (\forall x\in X.\ \forall y\in X.\ \forall z\in X.\ \langle d\langle x,z\rangle , A\langle d\langle x,y\rangle ,d\langle y,z\rangle \rangle \rangle \in r) \)
Definition of IsAmetric: \( \text{IsAmetric}(d,X,G,A,r) \equiv \) \( \text{IsApseudoMetric}(d,X,G,A,r) \wedge (\forall x\in X.\ \forall y\in X.\ d\langle x,y\rangle = \text{ TheNeutralElement}(G,A) \longrightarrow x=y) \)
lemma (in group0) group_is_loop: shows \( \text{IsAquasigroup}(G,P) \) and \( \text{IsAloop}(G,P) \)
lemma Order_ZF_1_L2:

assumes \( \text{IsLinOrder}(X,r) \)

shows \( \text{IsPartOrder}(X,r) \)
lemma (in group3) ord_transl_inv:

assumes \( a\leq b \), \( c\in G \)

shows \( a\cdot c \leq b\cdot c \) and \( c\cdot a \leq c\cdot b \)
lemma (in group3) ineq_cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq c\cdot b \)

shows \( a\leq c \)
lemma (in group3) OrderedGroup_ZF_1_L5AE:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq a\cdot c \)

shows \( b\leq c \)
Definition of IsAnOrdLoop: \( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)
lemma (in reals) reals_loop: shows \( \text{IsAnOrdLoop}(\mathbb{R} ,Add,ROrd) \)
lemma (in reals) dist_is_metric: shows \( dist : \mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R} ^+ \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = \vert x - y\vert \), \( \forall x\in \mathbb{R} .\ dist\langle x,x\rangle = 0 \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = dist\langle y,x\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ \vert x - z\vert \leq \vert x - y\vert + \vert y - z\vert \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ dist\langle x,z\rangle \leq dist\langle x, y\rangle + dist\langle y,z\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = 0 \longrightarrow x=y \), \( \text{IsApseudoMetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \), \( \text{IsAmetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \)
lemma (in ring1) OrdRing_ZF_1_L1: shows \( \text{IsAnOrdRing}(R,A,M,r) \)
lemma (in group3) pos_set_in_gr: shows \( G_+ \subseteq G^+ \) and \( G_+ \subseteq G \)
lemma ord_linear_subset:

assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)

shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \)
lemma lin_is_latt:

assumes \( r\subseteq L\times L \) and \( \text{IsLinOrder}(L,r) \)

shows \( r \text{ is a lattice on } L \)
lemma (in reals) pmetric_space_valid: shows \( pmetric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \)
lemma (in reals) pos_is_lattice: shows \( \text{IsLinOrder}(\mathbb{R} ,ROrd) \), \( \text{IsLinOrder}(\mathbb{R} _+,ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \), \( (ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \text{ is a lattice on } \mathbb{R} _+ \)
Definition of IsAlattice: \( r \text{ is a lattice on } L \equiv \text{IsJoinSemilattice}(L,r) \wedge \text{IsMeetSemilattice}(L,r) \)
lemma (in ring1) ordring_one_is_pos:

assumes \( 0 \neq 1 \)

shows \( 1 \in R_+ \)
Definition of RealTopology: \( \tau _\mathbb{R} \equiv \{\bigcup A.\ A \in Pow(\bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\})\} \)
theorem (in pmetric_space) pmetric_is_top:

assumes \( \text{IsMeetSemilattice}(L_+,r \cap L_+\times L_+) \), \( L_+\neq 0 \)

defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in L_+\} \)

defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)

shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)
44
56
9
9