Added a substantial new contribution from Liming Li, Zhiping Shi, Yon…

…g Guan,

Guohui Wang and Sha Ma, from Capital Normal University, Beijing: a theory of
geometric algebra (new subdirectory "Geometric_Algebra") with a multivector
structure (P,Q,R)multivector for formulating any geometric algebra G(P,Q,R)
with positive definite, negative definite and zero quadratic forms.

Also fixed some documentation bugs pointed out by Marco Maggesi, as well as
making a small tweak he suggested to remove warnings from the proof of
TC_CLOSED in "Library/rstc.ml".

Finally added a few other lemmas, the only slightly non-trivial ones being
KC_SPACE_PROD_TOPOLOGY_LEFT and KC_SPACE_PROD_TOPOLOGY_RIGHT, proving that
the product of a KC and a Hausdorff space is KC. New theorems:

        COMPACT_SPACE_CONTRACTIVE
        CONTINUOUS_MAP_INTO_EMPTY
        COUNTABLE_DIFF
        HAUSDORFF_SPACE_TOPSPACE_EMPTY
        HOMEOMORPHIC_SPACE_PROD_TOPOLOGY_SWAP
        KC_SPACE_EXPANSIVE
        KC_SPACE_PROD_TOPOLOGY_LEFT
        KC_SPACE_PROD_TOPOLOGY_RIGHT
        QUOTIENT_MAP_INTO_K_SPACE_EQ
        T0_SPACE_EXPANSIVE
        T1_SPACE_EXPANSIVE
        TOPOLOGY_FINER_SUBTOPOLOGY

CHANGES

@@ -8,6 +8,26 @@
   * page: https://github.com/jrh13/hol-light/commits/master         *
   * *****************************************************************
 
+Sat 20th Oct 2018       Geometric_Algebra [new directory]
+
+Added a new contribution from Liming Li, Zhiping Shi, Yong Guan, Guohui Wang
+and Sha Ma, from Capital Normal University, Beijing. This is a theory of 
+geometric algebra with a multivector structure (P,Q,R)multivector for
+formulating any geometric algebra G(P,Q,R) with positive definite, negative
+definite and zero quadratic forms.
+
+Fri 19th Oct 2018       Library/rstc.ml, Help/*
+
+Made a small change from Marco Maggesi to the proof of TC_CLOSED to remove
+warnings, as well as fixing a few documentation issues he pointed out.
+
+Fri 19th Oct 2018       Library/card.ml
+
+Added one trivial cardinal theorem where the FINITE analog is already there:
+
+COUNTABLE_DIFF =
+  |- !s t. COUNTABLE s ==> COUNTABLE (s DIFF t)
+
 Sun 23rd Sep 2018       sets.ml
 
 Added one trivial theorem, occasionally useful to avoid disturbing the

Geometric_Algebra/README

@@ -0,0 +1,8 @@
+Formulation of geometric algebra G(P,Q,R) with the multivector structure
+(P,Q,R)multivector, which can formulate positive definite, negative definite
+and zero quadratic forms.
+
+      (c) Copyright, Capital Normal University, China, 2018.
+  Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.
+
+     Distributed with HOL Light under the same license terms

Geometric_Algebra/make.ml

@@ -0,0 +1,9 @@
+(* ========================================================================= *)
+(* Load geometric algebra theory plus complex/quaternions application        *)
+(*                                                                           *)
+(*        (c) Copyright, Capital Normal University, China, 2018.             *)
+(*     Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.      *)
+(* ========================================================================= *)
+
+loadt "Geometric_Algebra/geometricalgebra.ml";;
+loadt "Geometric_Algebra/quaternions.ml";;

Geometric_Algebra/quaternions.ml

@@ -0,0 +1,138 @@
+(* ========================================================================= *)
+(* Complex numbers and quaternions in the geometric algebra theory.          *)
+(*                                                                           *)
+(*        (c) Copyright, Capital Normal University, China, 2018.             *)
+(*     Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.      *)
+(* ========================================================================= *)
+
+needs "Geometric_Algebra/geometricalgebra.ml";;
+needs "Quaternions/make.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Complexes in GA.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+let DIMINDEX_GA010 = prove
+ (`dimindex(:('0,'1,'0)geomalg) = dimindex(:2)`,
+  REWRITE_TAC[DIMINDEX_2; DIMINDEX_GEOMALG; PDIMINDEX_0; PDIMINDEX_1] THEN ARITH_TAC);;
+
+let COMPLEX_PRODUCT_GA010 = prove
+ (`!x y:real^('0,'1,'0)geomalg.
+     x * y =
+       (x $$ {} * y $$ {} - x $$ {1} * y $$ {1}) % mbasis {} +
+       (x $$ {} * y $$ {1} + x $$ {1} * y $$ {}) % mbasis {1}`,
+  REPEAT GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  REWRITE_TAC[PDIMINDEX_0; PDIMINDEX_1; ADD_0; ADD_SYM; NUMSEG_SING] THEN
+  REWRITE_TAC[prove(`{s | s SUBSET {1}} = {{}, {1}}`, REWRITE_TAC[POWERSET_CLAUSES] THEN SET_TAC[])] THEN
+  SIMP_TAC[VSUM_CLAUSES;FINITE_INSERT; FINITE_SING; IN_INSERT; IN_SING; NOT_EMPTY_INSERT; VSUM_SING] THEN
+  CONV_TAC GEOM_ARITH);;
+
+GEOM_ARITH `mbasis{1}:real^('0,'1,'0)geomalg * mbasis{1} = --mbasis{}`;;
+GEOM_ARITH `mbasis{1,2}:real^('2,'0,'0)geomalg * mbasis{1,2} = --mbasis{}`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Quaternions in GA.                                                        *)
+(* ------------------------------------------------------------------------- *)
+
+let DIMINDEX_GA020 = prove
+ (`dimindex(:('0,'2,'0)geomalg) = dimindex(:4)`,
+  REWRITE_TAC[DIMINDEX_4; DIMINDEX_GEOMALG; PDIMINDEX_0; PDIMINDEX_2] THEN ARITH_TAC);;
+
+let QUAT_PRODUCT_GA020 = prove
+ (`!x y:real^('0,'2,'0)geomalg.
+     x * y =
+       (x $$ {} * y $$ {} - x $$ {1} * y $$ {1} - x $$ {2} * y $$ {2} - x $$ {1,2} * y $$ {1,2}) % mbasis {} +
+       (x $$ {} * y $$ {1} + x $$ {1} * y $$ {} + x $$ {2} * y $$ {1,2} - x $$ {1,2} * y $$ {2}) % mbasis {1} +
+       (x $$ {} * y $$ {2} - x $$ {1} * y $$ {1,2} + x $$ {2} * y $$ {} + x $$ {1,2} * y $$ {1}) % mbasis {2} +
+       (x $$ {} * y $$ {1,2} + x $$ {1} * y $$ {2} - x $$ {2} * y $$ {1} + x $$ {1,2} * y $$ {}) % mbasis {1,2}`,
+  REPEAT GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  REWRITE_TAC[PDIMINDEX_0; PDIMINDEX_2; ADD_0; ADD_SYM] THEN
+  GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[TWO] THEN REWRITE_TAC[NUMSEG_CLAUSES] THEN REWRITE_TAC[ARITH; NUMSEG_SING] THEN
+  REWRITE_TAC[prove(`{s | s SUBSET {2,1}} = {{}, {1}, {2}, {1,2}}`,
+     REWRITE_TAC[POWERSET_CLAUSES] THEN REWRITE_TAC[EXTENSION] THEN
+     GEN_TAC THEN REWRITE_TAC[IN_UNION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN REWRITE_TAC[GSYM DISJ_ASSOC] THEN
+     MATCH_MP_TAC (TAUT `p1 = q1 /\ p2 = q2 ==> (p1 \/ p2) = (q1 \/q2)`) THEN CONJ_TAC THENL[SET_TAC[]; ALL_TAC] THEN
+     MATCH_MP_TAC (TAUT `p1 = q1 /\ p2 = q2 ==> (p1 \/ p2) = (q1 \/q2)`) THEN CONJ_TAC THEN
+     EQ_TAC THENL[SET_TAC[]; ALL_TAC; SET_TAC[]; ALL_TAC] THEN STRIP_TAC THENL
+      [EXISTS_TAC `{}:num->bool`; EXISTS_TAC `{}:num->bool`; EXISTS_TAC `{1}:num->bool`] THEN ASM_REWRITE_TAC[] THEN
+     CONJ_TAC THENL[SET_TAC[]; ALL_TAC] THEN DISJ2_TAC THEN EXISTS_TAC `{}:num->bool` THEN ASM_REWRITE_TAC[])] THEN
+  SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; FINITE_SING; IN_INSERT; IN_SING; NOT_EMPTY_INSERT; VSUM_SING] THEN
+  SIMP_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY] THEN
+  REWRITE_TAC[prove(`!a b:num. (!x. (x=a) <=> (x=b)) <=> (a=b)`, MESON_TAC[]);
+              prove(`!a b:num. (!x. (x=a) <=> (x=a) \/ (x=b)) <=> (a=b)`, MESON_TAC[]);
+              DISJ_SYM; ARITH_EQ] THEN
+  CONV_TAC GEOM_ARITH);;
+
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{1} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{2} = --mbasis {}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = --mbasis {}`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} = mbasis {1,2}`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = mbasis {1}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1} = mbasis {2}`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} = --(mbasis{2} * mbasis{1})`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis {2})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1} = --(mbasis{1} * mbasis{1,2})`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} * mbasis{1,2} = --mbasis{}`;;
+
+let geomalg_300_quat = new_definition
+`geomalg_300_quat (q:quat) =
+  (Re q) % mbasis{} +
+  (Im1 q) % mbasis{2,3} +
+  (Im2 q) % mbasis{1,2} +
+  (Im3 q) % (--(mbasis{1,3}:real^('3,'0,'0)geomalg))`;;
+
+let CNJ_QUAT = prove
+(`!q:quat. conjugation (geomalg_300_quat q) = geomalg_300_quat (cnj q)`,
+  GEN_TAC THEN REWRITE_TAC[conjugation; geomalg_300_quat; quat_cnj; QUAT_COMPONENTS] THEN
+  SIMP_TAC[GEOMALG_BETA; GEOMALG_EQ] THEN
+  REPEAT STRIP_TAC THEN
+  ASM_SIMP_TAC[VECTOR_NEG_MINUS1; GEOMALG_ADD_COMPONENT; GEOMALG_MUL_COMPONENT; MVBASIS_COMPONENT] THEN
+  REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
+  ASM_SIMP_TAC[MVBASIS_COMPONENT] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC);;
+
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)* mbasis{1,2} = --mbasis{}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)*(--mbasis{1,3}) = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis {1,2} = --mbasis{1,3}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)*(--mbasis{1,3}) = mbasis{2,3}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = mbasis{1,2}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis{2,3})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)*(--mbasis{1,3})= --(--mbasis{1,3} * mbasis{1,2})`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = --(mbasis{2,3} * --mbasis{1,3})`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{1,2} * --mbasis{1,3} = --mbasis{}`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Dual quaternions in GA.                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)* mbasis{1,2} = --mbasis{}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)*(--mbasis{1,3}) = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis {1,2} = --mbasis{1,3}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)*(--mbasis{1,3}) = mbasis{2,3}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = mbasis{1,2}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis{2,3})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)*(--mbasis{1,3})= --(--mbasis{1,3} * mbasis{1,2})`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = --(mbasis{2,3} * --mbasis{1,3})`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{1,2} * --mbasis{1,3} = --mbasis{}`;;
+GEOM_ARITH `mbasis{2,3}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = mbasis{1,2,3,4} * mbasis{2,3}`;;
+GEOM_ARITH `mbasis{1,2}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = mbasis{1,2,3,4} * mbasis{1,2}`;;
+GEOM_ARITH `--mbasis{1,3}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4}= mbasis{1,2,3,4}* --mbasis{1,3}`;;
+GEOM_ARITH `mbasis{1,2,3,4}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = vec 0`;;

Help/GEN_PART_MATCH.doc

@@ -40,6 +40,6 @@ difference with that function
 }
 
 \SEEALSO
-INST_TYPE, INST_TY_TERM, MATCH_MP, PART_MATCH, REWR_CONV, term_match.
+INST_TYPE, MATCH_MP, PART_MATCH, REWR_CONV, term_match.
 
 \ENDDOC

Help/NNFC_CONV.doc

@@ -34,7 +34,7 @@ A toplevel equivalence {p <=> q} is converted to {(p \/ ~q) /\ (~p \/ q)}. In
 general this ``splitting'' of equivalences is done with the expectation that
 the final formula may be put into conjunctive normal form (CNF), as a prelude
 to a proof (rather than refutation) procedure. An otherwise similar conversion
-{NNC_CONV} prefers a `disjunctive' splitting and is better suited for a term
+{NNF_CONV} prefers a `disjunctive' splitting and is better suited for a term
 that will later be translated to DNF for refutation.
 
 \SEEALSO

Help/PART_MATCH.doc

@@ -63,6 +63,6 @@ is not quite a higher-order pattern in the usual sense, consider the theorem:
 }
 
 \SEEALSO
-GEN_PART_MATCH, INST_TYPE, INST_TY_TERM, MATCH_MP, REWR_CONV, term_match.
+GEN_PART_MATCH, INST_TYPE, MATCH_MP, REWR_CONV, term_match.
 
 \ENDDOC

Help/subtract.doc

@@ -10,7 +10,7 @@ list, set.
 
 \DESCRIBE
 {subtract l1 l2} returns a list consisting of those elements of {l1} that do
-not appear in {l2}. If both lists are initially free of repetitions, this can 
+not appear in {l2}. If both lists are initially free of repetitions, this can
 be considered a set difference operation.
 
 \FAILURE
@@ -25,6 +25,6 @@ Never fails.
 }
 
 \SEEALSO
-setify, set_equal, union, intersect.
+setify, set_eq, union, intersect.
 
 \ENDDOC

LP_arith/Makefile

@@ -1,15 +1,14 @@
-
-
-CDDLIBPATH=/usr/local/lib
+CDDLIBPATH=/usr/lib/x86_64-linux-gnu
+CDDINCLUDEPATH=/usr/include/cdd
 
 GXX = g++
 CC = $(GXX)
 CCLD = $(CC)
 
 
-.SUFFIXES: .c .o
+.SUFFIXES: .c .o 
 
-COMPILE = $(CC) -O2 -DHAVE_LIBGMP=1 -DGMPRATIONAL -I. -I$(CDDLIBPATH)
+COMPILE = $(CC) -O2 -DHAVE_LIBGMP=1 -DGMPRATIONAL -I. -I$(CDDLIBPATH) -I$(CDDINCLUDEPATH)
 
 LINK = $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@
 
@@ -19,7 +18,7 @@ LINK = $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@
 all: cdd_cert
 
 cdd_cert: cdd_cert.o
-	$(LINK) cdd_cert.o $(CDDLIBPATH)/libcddgmp.a -l gmp
+	$(LINK) cdd_cert.o $(CDDLIBPATH)/libcddgmp.so -l gmp
 
 clean:
 	rm -f *~ *.o cdd_cert cdd_cert.exe

Library/card.ml

@@ -1617,6 +1617,10 @@ let COUNTABLE_DIFF_FINITE = prove
   SIMP_TAC[DIFF_EMPTY; SET_RULE `s DIFF (x INSERT t) = (s DIFF t) DELETE x`;
            COUNTABLE_DELETE]);;
 
+let COUNTABLE_DIFF = prove
+ (`!s t:A->bool. COUNTABLE s ==> COUNTABLE(s DIFF t)`,
+  MESON_TAC[COUNTABLE_SUBSET; SET_RULE `s DIFF t SUBSET s`]);;
+
 let COUNTABLE_CROSS = prove
  (`!s t. COUNTABLE s /\ COUNTABLE t ==> COUNTABLE(s CROSS t)`,
   REWRITE_TAC[COUNTABLE; ge_c; CROSS; GSYM mul_c] THEN

Library/rstc.ml

@@ -136,8 +136,9 @@ let TC_CLOSED = prove
  (`!R:A->A->bool. (TC R = R) <=> !x y z. R x y /\ R y z ==> R x z`,
   GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL
    [MESON_TAC[TC_RULES]; REPEAT STRIP_TAC] THEN
-  EQ_TAC THENL [RULE_INDUCT_TAC TC_INDUCT; ALL_TAC] THEN
-  ASM_MESON_TAC[TC_RULES]);;
+  EQ_TAC THENL
+   [RULE_INDUCT_TAC TC_INDUCT THEN ASM_MESON_TAC[];
+    MESON_TAC[TC_RULES]]);;
 
 let TC_IDEMP = prove
  (`!R:A->A->bool. TC(TC R) = TC R`,

Multivariate/complex_database.ml

@@ -2598,6 +2598,7 @@ theorems :=
 "COMPACT_SLICE",COMPACT_SLICE;
 "COMPACT_SPACE",COMPACT_SPACE;
 "COMPACT_SPACE_ALT",COMPACT_SPACE_ALT;
+"COMPACT_SPACE_CONTRACTIVE",COMPACT_SPACE_CONTRACTIVE;
 "COMPACT_SPACE_DISCRETE_TOPOLOGY",COMPACT_SPACE_DISCRETE_TOPOLOGY;
 "COMPACT_SPACE_EQ_BOLZANO_WEIERSTRASS",COMPACT_SPACE_EQ_BOLZANO_WEIERSTRASS;
 "COMPACT_SPACE_EQ_MCOMPLETE_TOTALLY_BOUNDED_IN",COMPACT_SPACE_EQ_MCOMPLETE_TOTALLY_BOUNDED_IN;
@@ -3582,6 +3583,7 @@ theorems :=
 "CONTINUOUS_MAP_IMAGE_SUBSET_TOPSPACE",CONTINUOUS_MAP_IMAGE_SUBSET_TOPSPACE;
 "CONTINUOUS_MAP_IMP_CLOSED_GRAPH",CONTINUOUS_MAP_IMP_CLOSED_GRAPH;
 "CONTINUOUS_MAP_INF",CONTINUOUS_MAP_INF;
+"CONTINUOUS_MAP_INTO_EMPTY",CONTINUOUS_MAP_INTO_EMPTY;
 "CONTINUOUS_MAP_INTO_FULLTOPOLOGY",CONTINUOUS_MAP_INTO_FULLTOPOLOGY;
 "CONTINUOUS_MAP_INTO_SUBTOPOLOGY",CONTINUOUS_MAP_INTO_SUBTOPOLOGY;
 "CONTINUOUS_MAP_INTO_TOPOLOGY_BASE",CONTINUOUS_MAP_INTO_TOPOLOGY_BASE;
@@ -4296,6 +4298,7 @@ theorems :=
 "COUNTABLE_DESCENDING_CHAIN",COUNTABLE_DESCENDING_CHAIN;
 "COUNTABLE_DESCENDING_CLOPEN_CHAIN",COUNTABLE_DESCENDING_CLOPEN_CHAIN;
 "COUNTABLE_DESCENDING_CLOPEN_IN_CHAIN",COUNTABLE_DESCENDING_CLOPEN_IN_CHAIN;
+"COUNTABLE_DIFF",COUNTABLE_DIFF;
 "COUNTABLE_DIFF_FINITE",COUNTABLE_DIFF_FINITE;
 "COUNTABLE_DISCONTINUITIES_IMP_BAIRE1",COUNTABLE_DISCONTINUITIES_IMP_BAIRE1;
 "COUNTABLE_DISJOINT_NONEMPTY_INTERIOR_SUBSETS",COUNTABLE_DISJOINT_NONEMPTY_INTERIOR_SUBSETS;
@@ -7642,6 +7645,7 @@ theorems :=
 "HAUSDORFF_SPACE_SING_INTERS_CLOSED",HAUSDORFF_SPACE_SING_INTERS_CLOSED;
 "HAUSDORFF_SPACE_SING_INTERS_OPENS",HAUSDORFF_SPACE_SING_INTERS_OPENS;
 "HAUSDORFF_SPACE_SUBTOPOLOGY",HAUSDORFF_SPACE_SUBTOPOLOGY;
+"HAUSDORFF_SPACE_TOPSPACE_EMPTY",HAUSDORFF_SPACE_TOPSPACE_EMPTY;
 "HD",HD;
 "HD_APPEND",HD_APPEND;
 "HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS",HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS;
@@ -7966,6 +7970,7 @@ theorems :=
 "HOMEOMORPHIC_SPACE_INFINITENESS",HOMEOMORPHIC_SPACE_INFINITENESS;
 "HOMEOMORPHIC_SPACE_PROD_TOPOLOGY",HOMEOMORPHIC_SPACE_PROD_TOPOLOGY;
 "HOMEOMORPHIC_SPACE_PROD_TOPOLOGY_SING",HOMEOMORPHIC_SPACE_PROD_TOPOLOGY_SING;
+"HOMEOMORPHIC_SPACE_PROD_TOPOLOGY_SWAP",HOMEOMORPHIC_SPACE_PROD_TOPOLOGY_SWAP;
 "HOMEOMORPHIC_SPACE_REFL",HOMEOMORPHIC_SPACE_REFL;
 "HOMEOMORPHIC_SPACE_SINGLETON_PRODUCT",HOMEOMORPHIC_SPACE_SINGLETON_PRODUCT;
 "HOMEOMORPHIC_SPACE_SYM",HOMEOMORPHIC_SPACE_SYM;
@@ -9781,9 +9786,12 @@ theorems :=
 "KC_SPACE_DISCRETE_TOPOLOGY",KC_SPACE_DISCRETE_TOPOLOGY;
 "KC_SPACE_EUCLIDEAN",KC_SPACE_EUCLIDEAN;
 "KC_SPACE_EUCLIDEANREAL",KC_SPACE_EUCLIDEANREAL;
+"KC_SPACE_EXPANSIVE",KC_SPACE_EXPANSIVE;
 "KC_SPACE_MTOPOLOGY",KC_SPACE_MTOPOLOGY;
 "KC_SPACE_PROD_TOPOLOGY",KC_SPACE_PROD_TOPOLOGY;
 "KC_SPACE_PROD_TOPOLOGY_ALT",KC_SPACE_PROD_TOPOLOGY_ALT;
+"KC_SPACE_PROD_TOPOLOGY_LEFT",KC_SPACE_PROD_TOPOLOGY_LEFT;
+"KC_SPACE_PROD_TOPOLOGY_RIGHT",KC_SPACE_PROD_TOPOLOGY_RIGHT;
 "KC_SPACE_RETRACTION_MAP_IMAGE",KC_SPACE_RETRACTION_MAP_IMAGE;
 "KC_SPACE_SUBTOPOLOGY",KC_SPACE_SUBTOPOLOGY;
 "KERNEL_MATRIX_INV",KERNEL_MATRIX_INV;
@@ -13546,6 +13554,7 @@ theorems :=
 "QUOTIENT_MAP_IMP_CONTINUOUS_CLOSED",QUOTIENT_MAP_IMP_CONTINUOUS_CLOSED;
 "QUOTIENT_MAP_IMP_CONTINUOUS_OPEN",QUOTIENT_MAP_IMP_CONTINUOUS_OPEN;
 "QUOTIENT_MAP_INTO_K_SPACE",QUOTIENT_MAP_INTO_K_SPACE;
+"QUOTIENT_MAP_INTO_K_SPACE_EQ",QUOTIENT_MAP_INTO_K_SPACE_EQ;
 "QUOTIENT_MAP_KOLMOGOROV_QUOTIENT",QUOTIENT_MAP_KOLMOGOROV_QUOTIENT;
 "QUOTIENT_MAP_KOLMOGOROV_QUOTIENT_GEN",QUOTIENT_MAP_KOLMOGOROV_QUOTIENT_GEN;
 "QUOTIENT_MAP_LIFT_EXISTS",QUOTIENT_MAP_LIFT_EXISTS;
@@ -16780,6 +16789,7 @@ theorems :=
 "T0_SPACE",T0_SPACE;
 "T0_SPACE_CLOSURE_OF_SING",T0_SPACE_CLOSURE_OF_SING;
 "T0_SPACE_DISCRETE_TOPOLOGY",T0_SPACE_DISCRETE_TOPOLOGY;
+"T0_SPACE_EXPANSIVE",T0_SPACE_EXPANSIVE;
 "T0_SPACE_KOLMOGOROV_QUOTIENT",T0_SPACE_KOLMOGOROV_QUOTIENT;
 "T0_SPACE_PRODUCT_TOPOLOGY",T0_SPACE_PRODUCT_TOPOLOGY;
 "T0_SPACE_PROD_TOPOLOGY",T0_SPACE_PROD_TOPOLOGY;
@@ -16798,6 +16808,7 @@ theorems :=
 "T1_SPACE_DERIVED_SET_OF_SING",T1_SPACE_DERIVED_SET_OF_SING;
 "T1_SPACE_EUCLIDEAN",T1_SPACE_EUCLIDEAN;
 "T1_SPACE_EUCLIDEANREAL",T1_SPACE_EUCLIDEANREAL;
+"T1_SPACE_EXPANSIVE",T1_SPACE_EXPANSIVE;
 "T1_SPACE_INTERS_OPEN_SUPERSETS",T1_SPACE_INTERS_OPEN_SUPERSETS;
 "T1_SPACE_MTOPOLOGY",T1_SPACE_MTOPOLOGY;
 "T1_SPACE_OPEN_IN_DELETE",T1_SPACE_OPEN_IN_DELETE;
@@ -16900,6 +16911,7 @@ theorems :=
 "TOPOLOGY_FINER_CLOSED_IN",TOPOLOGY_FINER_CLOSED_IN;
 "TOPOLOGY_FINER_CONTINUOUS_ID",TOPOLOGY_FINER_CONTINUOUS_ID;
 "TOPOLOGY_FINER_OPEN_ID",TOPOLOGY_FINER_OPEN_ID;
+"TOPOLOGY_FINER_SUBTOPOLOGY",TOPOLOGY_FINER_SUBTOPOLOGY;
 "TOPSPACE_DISCRETE_TOPOLOGY",TOPSPACE_DISCRETE_TOPOLOGY;
 "TOPSPACE_EUCLIDEAN",TOPSPACE_EUCLIDEAN;
 "TOPSPACE_EUCLIDEANREAL",TOPSPACE_EUCLIDEANREAL;