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. Note we define the (real) natural numbers \(\mathbb{N}\) as starting from one.
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 \( \frac{1}{2} \equiv 2 ^{-1} \)
defines \( \sum s \equiv \text{Fold}(Add, 0 ,s) \)
defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)
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) \)
defines \( \mathbb{N} \equiv \bigcap \{N \in Pow(\mathbb{R} ).\ 1 \in N \wedge (\forall n.\ n\in N \longrightarrow n + 1 \in N)\} \)
defines \( \prod s \equiv \text{Fold}(Mul,1 ,s) \)
defines \( x^{n} \equiv \prod \{\langle k,x\rangle .\ k\in n\} \)
defines \( A \text{ has a supremum } \equiv \text{HasAsupremum}(ROrd,A) \)
defines \( A \text{ has an infimum } \equiv \text{HasAnInfimum}(ROrd,A) \)
defines \( sup(A) \equiv \text{Supremum}(ROrd,A) \)
defines \( inf(A) \equiv \text{Infimum}(ROrd,A) \)
The assumptions 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
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
}
ultimately show \( \text{IsAnOrdLoop}(\mathbb{R} ,Add,ROrd) \) unfolding IsAnOrdLoop_def
qed
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) \)
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)The assumptions of the metric_space locale hold in the reals locale.
lemma (in reals) metric_space_valid:
shows \( metric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \)proof have \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = 0 \longrightarrow x=y \) using dist_is_metric(9) unfolding IsAmetric_def
then show \( thesis \) unfolding metric_space_def, metric_space_axioms_def using pmetric_space_valid
qed
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
qed
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
Of course the set of positive real numbers is nonempty as one is there.
lemma (in reals) pos_non_empty:
shows \( \mathbb{R} _+\neq 0 \) using R_are_reals, ordring_one_is_pos unfolding IsAmodelOfReals_def, IsAnOrdField_defWe say that a relation \(r\) \( down-directs \) a set \(R\) if every two-element subset of \(R\) has a lower bound. The next lemma states that the natural order relation on real numbers down-directs the set of positive reals.
lemma (in reals) rord_down_directs:
shows \( ROrd \text{ down-directs } \mathbb{R} _+ \) using pos_is_lattice(3), pos_non_empty, meet_down_directs, down_dir_mono unfolding IsAlattice_defWe define the topology on reals as the metric topology coming from the dist metric (i.e. consisting of the unions of open disks).
definition (in reals)
\( \tau _\mathbb{R} \equiv \text{MetricTopology}(\mathbb{R} ,\mathbb{R} ,Add,ROrd,dist) \)
A more explicit definition of the real topology in notation used in the reals context.
lemma (in reals) real_toplology_def_alt:
shows \( \tau _\mathbb{R} = \{\bigcup A.\ A \in Pow(\bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\})\} \) unfolding MetricTopology_def, RealTopology_defReal numbers form a Hausdorff topological space with topology generated by open disks.
theorem (in reals) reals_is_top:
shows \( \tau _\mathbb{R} \text{ is a topology } \), \( \bigcup \tau _\mathbb{R} = \mathbb{R} \), \( \tau _\mathbb{R} \text{ is }T_2 \) using rord_down_directs, metric_space_valid, pmetric_space_valid, pmetric_is_top, metric_top_carrier, metric_space_T2 unfolding RealTopology_defThe definition of the model of real numbers requires that every nonempty set that is bounded above has a supremum. In the next theorem we show that every nonempty sets that is bounded below has an infimum.
lemma (in reals) bounded_below_has_inf:
assumes \( A\neq \emptyset \), \( \text{IsBoundedBelow}(A,ROrd) \)
shows \( \text{HasAnInfimum}(ROrd,A) \) using R_are_reals, assms, complete_bounded_below_inf unfolding IsAmodelOfReals_def, IsAnOrdField_def, IsAnOrdRing_def, IsLinOrder_defEvery nonempty bounded above subset of reals has a supremum. This follows straight from the definition of (a model of) real numbers, included here as dual to bounded_below_has_inf.
lemma (in reals) bounded_above_has_sup:
assumes \( A\neq \emptyset \), \( \text{IsBoundedAbove}(A,ROrd) \)
shows \( \text{HasAsupremum}(ROrd,A) \) using R_are_reals, assms unfolding IsAmodelOfReals_def, IsComplete_def, HasAsupremum_defEach nonempty set of nonnegative reals is bounded below. This is really an ordered loop property, we rewrite it here in the reals context for easy reference.
lemma (in reals) nonneg_reals_bound_below:
assumes \( A\subseteq \mathbb{R} ^+ \)
shows \( \text{IsBoundedBelow}(A,ROrd) \) using assms, loop1_valid_in_group3, nonnegative_bounded_belowEach nonempty set of nonnegative numbers is bounded below, hence has an infimum.
lemma (in reals) nonnegative_have_inf:
assumes \( A\neq \emptyset \), \( A\subseteq \mathbb{R} ^+ \)
shows \( \text{HasAnInfimum}(ROrd,A) \) using assms, nonneg_reals_bound_below, bounded_below_has_infFor sets that are bounded below we have \(\inf(A+B) = (\inf A) + (\inf B)\) This is an ordered loop property, we bring it here via ordered groups.
theorem (in reals) inf_sum_sum_inf:
assumes \( A\neq \emptyset \), \( \text{IsBoundedBelow}(A,ROrd) \), \( B\neq \emptyset \), \( \text{IsBoundedBelow}(B,ROrd) \)
shows \( \text{HasAnInfimum}(ROrd,\{x + y.\ \langle x,y\rangle \in A\times B\}) \) and \( inf(A) + inf(B) = inf(\{x + y.\ \langle x,y\rangle \in A\times B\}) \) using assms, bounded_below_has_inf, loop1_valid_in_group3, ordloop_inf_sum_sum_infFor sets that are bounded above we have \(\sup(A+B) = (\sup A) + (\inf B)\) This is an ordered loop property, we bring it here via ordered groups.
theorem (in reals) sup_sum_sum_sup:
assumes \( A\neq \emptyset \), \( \text{IsBoundedAbove}(A,ROrd) \), \( B\neq \emptyset \), \( \text{IsBoundedAbove}(B,ROrd) \)
shows \( \text{HasAsupremum}(ROrd,\{x + y.\ \langle x,y\rangle \in A\times B\}) \) and \( sup(A) + sup(B) = sup(\{x + y.\ \langle x,y\rangle \in A\times B\}) \) using assms, bounded_above_has_sup, loop1_valid_in_group3, ordloop_sup_sum_sum_supIn particular \(\inf(A+B) = (\inf A) + (\inf B)\) holds for subsets of nonnegative reals.
corollary (in reals) nonneg_inf_sum_inf:
assumes \( A\neq \emptyset \), \( A\subseteq \mathbb{R} ^+ \), \( B\neq \emptyset \), \( B\subseteq \mathbb{R} ^+ \)
shows \( \text{HasAnInfimum}(ROrd,\{x + y.\ \langle x,y\rangle \in A\times B\}) \) and \( inf(A) + inf(B) = inf(\{x + y.\ \langle x,y\rangle \in A\times B\}) \) using assms, nonneg_reals_bound_below, inf_sum_sum_infIn the context of real numbers having an infimum is the same as being nonempty and bounded below.
lemma (in reals) has_inf_is_nempty_bb:
shows \( \text{HasAnInfimum}(ROrd,A) \longleftrightarrow A\neq \emptyset \wedge \text{IsBoundedBelow}(A,ROrd) \) using linord, set_inf_not_empty, has_inf_bounded_below, bounded_below_has_inf unfolding IsLinOrder_defIn the context of real numbers having a supremum is the same as being nonempty and bounded above.
lemma (in reals) has_sup_is_nempty_ba:
shows \( \text{HasAsupremum}(ROrd,A) \longleftrightarrow A\neq \emptyset \wedge \text{IsBoundedAbove}(A,ROrd) \) using linord, set_sup_not_empty, has_sup_bounded_above, bounded_above_has_sup unfolding IsLinOrder_def 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 reals) field1_is_valid: shows \( field1(\mathbb{R} , Add, Mul,ROrd) \)
lemma (in group3) OrderedGroup_ZF_1_L1: shows \( group0(G,P) \)
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 \( \vert a\vert \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 \( \vert 1 \vert = 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 \( \vert a^{-1}\vert = \vert a\vert \) lemma (in group3) OrderedGroup_ZF_3_L3D:
assumes \( a\in G \) and \( \vert a\vert = 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 \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \)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 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 reals) pmetric_space_valid: shows \( pmetric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \)
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 ring1) ordring_one_is_pos:
assumes \( 0 \neq 1 \)
shows \( 1 \in R_+ \), \( 0 \lt 1 \) 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} _+ \)
lemma (in reals) pos_non_empty: shows \( \mathbb{R} _+\neq 0 \)
lemma meet_down_directs:
assumes \( \text{IsMeetSemilattice}(L,r) \), \( L\neq 0 \)
shows \( r \text{ down-directs } L \) lemma down_dir_mono:
assumes \( r \text{ down-directs } X \), \( r\subseteq R \)
shows \( R \text{ down-directs } X \)Definition of IsAlattice:
\( r \text{ is a lattice on } L \equiv \text{IsJoinSemilattice}(L,r) \wedge \text{IsMeetSemilattice}(L,r) \)
Definition of MetricTopology:
\( \text{MetricTopology}(X,L,A,r,d) \equiv \{\bigcup \mathcal{A} .\ \mathcal{A} \in Pow(\bigcup c\in X.\ \{ \text{Disk}(X,d,r,c,R).\ R\in \text{PositiveSet}(L,A,r)\})\} \)
Definition of RealTopology:
\( \tau _\mathbb{R} \equiv \text{MetricTopology}(\mathbb{R} ,\mathbb{R} ,Add,ROrd,dist) \)
lemma (in reals) rord_down_directs: shows \( ROrd \text{ down-directs } \mathbb{R} _+ \)
lemma (in reals) metric_space_valid: shows \( metric\_space(\mathbb{R} ,Add, ROrd,dist,\mathbb{R} ) \)
theorem (in pmetric_space) pmetric_is_top:
assumes \( r \text{ down-directs } L_+ \)
shows \( \tau \text{ is a topology } \) theorem (in pmetric_space) metric_top_carrier:
assumes \( r \text{ down-directs } L_+ \)
shows \( \bigcup \tau = X \) theorem (in metric_space) metric_space_T2:
assumes \( r \text{ down-directs } L_+ \)
shows \( \tau \text{ is }T_2 \) theorem complete_bounded_below_inf:
assumes \( r\subseteq X\times X \), \( \text{antisym}(r) \), \( r \text{ is complete } \), \( A\neq \emptyset \), \( \text{IsBoundedBelow}(A,r) \)
shows \( \text{HasAnInfimum}(r,A) \) and \( \text{Infimum}(r,A) = \text{Maximum}(r,\{y\in X.\ \forall x\in A.\ \langle y,x\rangle \in r\}) \), \( \text{Infimum}(r,A) = \text{Supremum}(r,\{y\in X.\ \forall x\in A.\ \langle y,x\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 IsComplete:
\( r \text{ is complete } \equiv \)
\( \forall A.\ \text{IsBoundedAbove}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
Definition of HasAsupremum:
\( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
lemma (in group3) loop1_valid_in_group3: shows \( loop1(G,P,r) \)
lemma (in loop1) nonnegative_bounded_below:
assumes \( B\subseteq L^+ \)
shows \( \text{IsBoundedBelow}(B,r) \) lemma (in reals) nonneg_reals_bound_below:
assumes \( A\subseteq \mathbb{R} ^+ \)
shows \( \text{IsBoundedBelow}(A,ROrd) \) lemma (in reals) bounded_below_has_inf:
assumes \( A\neq \emptyset \), \( \text{IsBoundedBelow}(A,ROrd) \)
shows \( \text{HasAnInfimum}(ROrd,A) \) theorem (in loop1) ordloop_inf_sum_sum_inf:
assumes \( \text{HasAnInfimum}(r,B) \) and \( \text{HasAnInfimum}(r,C) \)
shows \( \text{HasAnInfimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Infimum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Infimum}(r,B) + \text{Infimum}(r,C) \) lemma (in reals) bounded_above_has_sup:
assumes \( A\neq \emptyset \), \( \text{IsBoundedAbove}(A,ROrd) \)
shows \( \text{HasAsupremum}(ROrd,A) \) theorem (in loop1) ordloop_sup_sum_sum_sup:
assumes \( \text{HasAsupremum}(r,B) \) and \( \text{HasAsupremum}(r,C) \)
shows \( \text{HasAsupremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) \) and \( \text{Supremum}(r,\{x + y.\ \langle x,y\rangle \in B\times C\}) = \text{Supremum}(r,B) + \text{Supremum}(r,C) \) theorem (in reals) inf_sum_sum_inf:
assumes \( A\neq \emptyset \), \( \text{IsBoundedBelow}(A,ROrd) \), \( B\neq \emptyset \), \( \text{IsBoundedBelow}(B,ROrd) \)
shows \( \text{HasAnInfimum}(ROrd,\{x + y.\ \langle x,y\rangle \in A\times B\}) \) and \( inf(A) + inf(B) = inf(\{x + y.\ \langle x,y\rangle \in A\times B\}) \) lemma set_inf_not_empty:
assumes \( \text{HasAnInfimum}(r,A) \)
shows \( A\neq \emptyset \) lemma has_inf_bounded_below:
assumes \( \text{antisym}(r) \) and \( \text{HasAnInfimum}(r,A) \)
shows \( \text{IsBoundedBelow}(A,r) \) lemma set_sup_not_empty:
assumes \( \text{HasAsupremum}(r,A) \)
shows \( A\neq \emptyset \) lemma has_sup_bounded_above:
assumes \( \text{antisym}(r) \) and \( \text{HasAsupremum}(r,A) \)
shows \( \text{IsBoundedAbove}(A,r) \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
