Added a number of general topology theorems, with a particular emphasis

on those placing a minimal cardinality on connected or path-connected
sets in conjunction with various separation axioms:

        CARD_EQ_OPEN_CLOSED_IN_SETS
        CARD_LE_TOPSPACE_CLOSED_SETS
        CARD_LE_TOPSPACE_OPEN_SETS
        CONNECTED_IN_IMP_PERFECT
        CONNECTED_IN_IMP_PERFECT_GEN
        CONNECTED_SPACE_IMP_CARD_GE
        CONNECTED_SPACE_IMP_CARD_GE_ALT
        CONNECTED_SPACE_IMP_CARD_GE_GEN
        CONNECTED_SPACE_IMP_INFINITE
        CONNECTED_SPACE_IMP_INFINITE_ALT
        CONNECTED_SPACE_IMP_INFINITE_GEN
        CONTINUOUS_EXTENSION_OF_PROPER_MAP_FROM_SUBTOPOLOGY
        EMBEDDING_MAP_ON_DENSE_SUBTOPOLOGY
        INFINITE_PERFECT_SET
        INFINITE_PERFECT_SET_GEN
        KC_SPACE_PROD_TOPOLOGY_GEN
        PATH_CONNECTED_SPACE_IMP_CARD_GE
        RETRACTION_MAPS_SUBTOPOLOGIES
        RETRACTION_MAP_INTO_SUBTOPOLOGY

Multivariate/complex_database.ml

@@ -1483,6 +1483,7 @@ theorems :=
 "CARD_EQ_NONEMPTY_INTERIOR",CARD_EQ_NONEMPTY_INTERIOR;
 "CARD_EQ_NSUM",CARD_EQ_NSUM;
 "CARD_EQ_OPEN",CARD_EQ_OPEN;
+"CARD_EQ_OPEN_CLOSED_IN_SETS",CARD_EQ_OPEN_CLOSED_IN_SETS;
 "CARD_EQ_OPEN_IN",CARD_EQ_OPEN_IN;
 "CARD_EQ_OPEN_IN_AFFINE",CARD_EQ_OPEN_IN_AFFINE;
 "CARD_EQ_OPEN_SETS",CARD_EQ_OPEN_SETS;
@@ -1603,6 +1604,8 @@ theorems :=
 "CARD_LE_SQUARE",CARD_LE_SQUARE;
 "CARD_LE_SUBPOWERSET",CARD_LE_SUBPOWERSET;
 "CARD_LE_SUBSET",CARD_LE_SUBSET;
+"CARD_LE_TOPSPACE_CLOSED_SETS",CARD_LE_TOPSPACE_CLOSED_SETS;
+"CARD_LE_TOPSPACE_OPEN_SETS",CARD_LE_TOPSPACE_OPEN_SETS;
 "CARD_LE_TOTAL",CARD_LE_TOTAL;
 "CARD_LE_TRANS",CARD_LE_TRANS;
 "CARD_LE_UNIONS",CARD_LE_UNIONS;
@@ -3241,6 +3244,8 @@ theorems :=
 "CONNECTED_IN_EUCLIDEANREAL",CONNECTED_IN_EUCLIDEANREAL;
 "CONNECTED_IN_EUCLIDEANREAL_INTERVAL",CONNECTED_IN_EUCLIDEANREAL_INTERVAL;
 "CONNECTED_IN_EUCLIDEAN_COMPLEMENTS",CONNECTED_IN_EUCLIDEAN_COMPLEMENTS;
+"CONNECTED_IN_IMP_PERFECT",CONNECTED_IN_IMP_PERFECT;
+"CONNECTED_IN_IMP_PERFECT_GEN",CONNECTED_IN_IMP_PERFECT_GEN;
 "CONNECTED_IN_INTERMEDIATE_CLOSURE_OF",CONNECTED_IN_INTERMEDIATE_CLOSURE_OF;
 "CONNECTED_IN_INTER_FRONTIER_OF",CONNECTED_IN_INTER_FRONTIER_OF;
 "CONNECTED_IN_MONOTONE_QUOTIENT_MAP_PREIMAGE",CONNECTED_IN_MONOTONE_QUOTIENT_MAP_PREIMAGE;
@@ -3320,7 +3325,13 @@ theorems :=
 "CONNECTED_SPACE_IFF_COMPONENTS_EQ",CONNECTED_SPACE_IFF_COMPONENTS_EQ;
 "CONNECTED_SPACE_IFF_COMPONENTS_SUBSET_SING",CONNECTED_SPACE_IFF_COMPONENTS_SUBSET_SING;
 "CONNECTED_SPACE_IFF_CONNECTED_COMPONENT",CONNECTED_SPACE_IFF_CONNECTED_COMPONENT;
+"CONNECTED_SPACE_IMP_CARD_GE",CONNECTED_SPACE_IMP_CARD_GE;
+"CONNECTED_SPACE_IMP_CARD_GE_ALT",CONNECTED_SPACE_IMP_CARD_GE_ALT;
+"CONNECTED_SPACE_IMP_CARD_GE_GEN",CONNECTED_SPACE_IMP_CARD_GE_GEN;
 "CONNECTED_SPACE_IMP_CONNECTED_COMPONENT_OF",CONNECTED_SPACE_IMP_CONNECTED_COMPONENT_OF;
+"CONNECTED_SPACE_IMP_INFINITE",CONNECTED_SPACE_IMP_INFINITE;
+"CONNECTED_SPACE_IMP_INFINITE_ALT",CONNECTED_SPACE_IMP_INFINITE_ALT;
+"CONNECTED_SPACE_IMP_INFINITE_GEN",CONNECTED_SPACE_IMP_INFINITE_GEN;
 "CONNECTED_SPACE_MONOTONE_QUOTIENT_MAP_PREIMAGE",CONNECTED_SPACE_MONOTONE_QUOTIENT_MAP_PREIMAGE;
 "CONNECTED_SPACE_PRODUCT_TOPOLOGY",CONNECTED_SPACE_PRODUCT_TOPOLOGY;
 "CONNECTED_SPACE_PROD_TOPOLOGY",CONNECTED_SPACE_PROD_TOPOLOGY;
@@ -3501,6 +3512,7 @@ theorems :=
 "CONTINUOUS_EQ_COMPACT_CONNECTED_PRESERVING_GEN",CONTINUOUS_EQ_COMPACT_CONNECTED_PRESERVING_GEN;
 "CONTINUOUS_EQ_COMPACT_PATH_CONNECTED_PRESERVING",CONTINUOUS_EQ_COMPACT_PATH_CONNECTED_PRESERVING;
 "CONTINUOUS_EQ_UNIFORMLY_CONTINUOUS_MAP",CONTINUOUS_EQ_UNIFORMLY_CONTINUOUS_MAP;
+"CONTINUOUS_EXTENSION_OF_PROPER_MAP_FROM_SUBTOPOLOGY",CONTINUOUS_EXTENSION_OF_PROPER_MAP_FROM_SUBTOPOLOGY;
 "CONTINUOUS_FINITE_RANGE_CONSTANT",CONTINUOUS_FINITE_RANGE_CONSTANT;
 "CONTINUOUS_FINITE_RANGE_CONSTANT_EQ",CONTINUOUS_FINITE_RANGE_CONSTANT_EQ;
 "CONTINUOUS_FROM_CLOSED_GRAPH",CONTINUOUS_FROM_CLOSED_GRAPH;
@@ -5354,6 +5366,7 @@ theorems :=
 "EMBEDDING_MAP_INL",EMBEDDING_MAP_INL;
 "EMBEDDING_MAP_INTO_EUCLIDEANREAL",EMBEDDING_MAP_INTO_EUCLIDEANREAL;
 "EMBEDDING_MAP_IN_SUBTOPOLOGY",EMBEDDING_MAP_IN_SUBTOPOLOGY;
+"EMBEDDING_MAP_ON_DENSE_SUBTOPOLOGY",EMBEDDING_MAP_ON_DENSE_SUBTOPOLOGY;
 "EMBEDDING_MAP_ON_EMPTY",EMBEDDING_MAP_ON_EMPTY;
 "EMPTY",EMPTY;
 "EMPTY_AS_INTERVAL",EMPTY_AS_INTERVAL;
@@ -8643,6 +8656,8 @@ theorems :=
 "INFINITE_IRRATIONAL_IN_RANGE",INFINITE_IRRATIONAL_IN_RANGE;
 "INFINITE_NONEMPTY",INFINITE_NONEMPTY;
 "INFINITE_OPEN_IN",INFINITE_OPEN_IN;
+"INFINITE_PERFECT_SET",INFINITE_PERFECT_SET;
+"INFINITE_PERFECT_SET_GEN",INFINITE_PERFECT_SET_GEN;
 "INFINITE_RATIONAL",INFINITE_RATIONAL;
 "INFINITE_RATIONAL_IN_RANGE",INFINITE_RATIONAL_IN_RANGE;
 "INFINITE_SIMPLE_PATH_IMAGE",INFINITE_SIMPLE_PATH_IMAGE;
@@ -9936,6 +9951,7 @@ theorems :=
 "KC_SPACE_PERFECT_MAP_IMAGE",KC_SPACE_PERFECT_MAP_IMAGE;
 "KC_SPACE_PROD_TOPOLOGY",KC_SPACE_PROD_TOPOLOGY;
 "KC_SPACE_PROD_TOPOLOGY_ALT",KC_SPACE_PROD_TOPOLOGY_ALT;
+"KC_SPACE_PROD_TOPOLOGY_GEN",KC_SPACE_PROD_TOPOLOGY_GEN;
 "KC_SPACE_PROD_TOPOLOGY_LEFT",KC_SPACE_PROD_TOPOLOGY_LEFT;
 "KC_SPACE_PROD_TOPOLOGY_RIGHT",KC_SPACE_PROD_TOPOLOGY_RIGHT;
 "KC_SPACE_PROPER_MAP_IMAGE",KC_SPACE_PROPER_MAP_IMAGE;
@@ -13145,6 +13161,7 @@ theorems :=
 "PATH_CONNECTED_SPACE_IFF_COMPONENTS_EQ",PATH_CONNECTED_SPACE_IFF_COMPONENTS_EQ;
 "PATH_CONNECTED_SPACE_IFF_COMPONENTS_SUBSET_SING",PATH_CONNECTED_SPACE_IFF_COMPONENTS_SUBSET_SING;
 "PATH_CONNECTED_SPACE_IFF_PATH_COMPONENT",PATH_CONNECTED_SPACE_IFF_PATH_COMPONENT;
+"PATH_CONNECTED_SPACE_IMP_CARD_GE",PATH_CONNECTED_SPACE_IMP_CARD_GE;
 "PATH_CONNECTED_SPACE_IMP_PATH_COMPONENT_OF",PATH_CONNECTED_SPACE_IMP_PATH_COMPONENT_OF;
 "PATH_CONNECTED_SPACE_PATH_COMPONENT_SET",PATH_CONNECTED_SPACE_PATH_COMPONENT_SET;
 "PATH_CONNECTED_SPACE_PRODUCT_TOPOLOGY",PATH_CONNECTED_SPACE_PRODUCT_TOPOLOGY;
@@ -15536,10 +15553,12 @@ theorems :=
 "RETRACTION_MAPS_EUCLIDEAN",RETRACTION_MAPS_EUCLIDEAN;
 "RETRACTION_MAPS_KOLMOGOROV_QUOTIENT",RETRACTION_MAPS_KOLMOGOROV_QUOTIENT;
 "RETRACTION_MAPS_SECTION_IMAGE",RETRACTION_MAPS_SECTION_IMAGE;
+"RETRACTION_MAPS_SUBTOPOLOGIES",RETRACTION_MAPS_SUBTOPOLOGIES;
 "RETRACTION_MAPS_TO_RETRACT_MAPS",RETRACTION_MAPS_TO_RETRACT_MAPS;
 "RETRACTION_MAP_COMPOSE",RETRACTION_MAP_COMPOSE;
 "RETRACTION_MAP_EQ",RETRACTION_MAP_EQ;
 "RETRACTION_MAP_FST",RETRACTION_MAP_FST;
+"RETRACTION_MAP_INTO_SUBTOPOLOGY",RETRACTION_MAP_INTO_SUBTOPOLOGY;
 "RETRACTION_MAP_KOLMOGOROV_QUOTIENT",RETRACTION_MAP_KOLMOGOROV_QUOTIENT;
 "RETRACTION_MAP_PRODUCT_PROJECTION",RETRACTION_MAP_PRODUCT_PROJECTION;
 "RETRACTION_MAP_SND",RETRACTION_MAP_SND;