HOL html

Files Index

Theorems Index

C (theorems)

C5_QX_NEXT_TO_QY
C5_QX_NEXT_TO_QY_LEFT
C5_QY_ALONG_NOT_SMALL1
C5_QY_ALONG_NOT_SMALL2
CADD_0_n
CADD_n_0
CARD2
CARD2_EDGEX
CARD3
CARD4
CARD4_ALL_DISTINCT
CARD4_IMP_DISTINCT
CARD4_IN_PAIRS
CARD5
CARD5_1074_LE_QYI
CARD5_LT_1074_QYI
CARD_1_IMP_SING
CARD_2_FAN
CARD_2_IMP_DOUBLE
CARD_3
CARD_3_SUBSET
CARD_ADD1_LE
CARD_ATLEAST_1
CARD_ATLEAST_2
CARD_AT_LEAST3
CARD_BOUNDARY_INT_BALL_BOUND
CARD_BOUNDARY_INT_BALL_BOUND_1
CARD_CLAUSES2
CARD_CLAUSES_IMP
CARD_DART_FANADD
CARD_DART_OF_HYP
CARD_DELETE_CHOICE
CARD_DISJOINT
CARD_EDGEX_LE_16
CARD_EDGE_SET_FAN
CARD_EQUATION
CARD_EQUI_FF_SYM_0
CARD_EQ_DIM
CARD_EXISTS_2
CARD_E_GT1_EQ_CARD_E_PRIME
CARD_FACE_GT_1
CARD_FACE_ISO
CARD_FACE_OF_LIST
CARD_FACE_SET_EQ_3_FULLY_SURROUNDED_FAN
CARD_FACE_SET_EQ_3_FULLY_SURROUNDED_FAN1
CARD_FACE_SET_GE_3_FULLY_SURROUNDED_FAN
CARD_FACE_SY
CARD_FF_EQ_CARD_SLICE_FF
CARD_FF_EQ_SCS_K_3
CARD_FF_EQ_V3_DEFOR_DEFORMATION
CARD_FF_EQ_V3_DEFOR_DEFORMATION_MK
CARD_FF_EQ_WW_DEFORMATION
CARD_FF_GT1_FF_SUBSET
CARD_FINITE_SERIES_EQ
CARD_FINITE_SERIES_LE
CARD_F_SY_EQ
CARD_F_SY_IN_B_SY
CARD_GE_DIM_INDEPENDENT
CARD_GE_REFL
CARD_GT1_EE_OF_HYP_E_PRIME_EQ
CARD_GT1_IMP_AZIM_FAN_EQ_AZIM
CARD_GT1_IMP_AZIM_FAN_EQ_DIHV
CARD_IMAGE_F_SY_EQ
CARD_IMAGE_INJ2
CARD_INJ_LE
CARD_INSERT_GE_AND_LE
CARD_INSERT_INTER
CARD_INSERT_INTER_ALT
CARD_IS_LEAST_CYCLE
CARD_ITER_K_EK_IMP_DIST
CARD_I_SY_LT_3
CARD_KS_EQ_K_EQ_ALL_LE
CARD_K_ELMS_EQ_K_IMP_ALL_DISTINCT
CARD_K_FIRST_ELMS_EQ_K
CARD_LE_3
CARD_LE_DIM_SPANNING
CARD_LIST_4_klemma
CARD_LIST_klemma
CARD_LIST_klemma_2
CARD_LT_KT_LE_ADDT
CARD_MCELL_CONTAINS_POINT_klemma
CARD_MINUS_DIFF_TWO_SET
CARD_MINUS_ONE
CARD_MOD_NUMSEG
CARD_NODE_HYPERMAP_OF_FAN
CARD_NODE_ISO
CARD_NODE_SY
CARD_N_FIRST_ELMS_UNDUCTIVE
CARD_ORBITS_EDGE_FAN_LE
CARD_ORBITS_SIGMA_FAN_LE
CARD_PAIR_SYM_0
CARD_RECUSIVE_EQ
CARD_SCS_M_4I1
CARD_SCS_M_4I2
CARD_SCS_M_5I1
CARD_SCS_M_5M2
CARD_SCS_M_6M1
CARD_SET2
CARD_SET_OF_EDGE_GT_1_IMP_CARD_FACE_GE_3
CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON
CARD_SET_OF_LIST_ALL_DISTINCT
CARD_SET_OF_LIST_EQ_LENGTH_IMP_ALL_DISTINCT
CARD_SET_OF_LIST_FACE
CARD_SET_OF_LIST_LE
CARD_SET_OF_LIST_NODE
CARD_SET_OF_ORBITS_POINTS_FAN
CARD_SIGMA_FAN
CARD_SING
CARD_SINGLETON
CARD_SLICEF
CARD_SLICEV
CARD_SLICEV_LT
CARD_SLICE_EQ
CARD_SLICE_FF_LE_3
CARD_SLICE_LE
CARD_SLICE_LE1
CARD_STDBASIS
CARD_SYM_0
CARD_TWO_ELEMENTS
CARD_UNION_EDGES_LE
CARD_UNION_EQ
CARD_UNION_NOT_DISTJ_LT
CARD_VERTEX_GE_3_LOCAL_FAN
CARD_V_EQ_SCS_K
CARD_V_EQ_SCS_K1
CARD_V_TWO_HAFL_CIRCLE
CARD_W_AS_ALL_LESS_THAN_PERIODIC
CARD_W_IS_THE_PERIODIC
CARD_faces1
CARD_in_face
CARD_in_node
CARD_nodes
CART2_EQ
CART_EQ_3
CASES_OF_Q_SYS
CASE_3Q1H
CASE_FAN_FINITE
CASE_FAN_INDEPENDENCE
CASE_FAN_INTERSECTION
CASE_FAN_ORIGIN
CASE_PSORT
CAUCHY_FAN
CAUCHY_IMP_BOUNDED_FAN
CAYLEYR_5POINTS
CBALL_SUBSET_VORONOI_CLOSED
CC_2_PROPS
CC_3_AZIM_LT_PI_COPLANAR
CC_3_PROPS
CC_3_SUM_SET
CC_3_SUM_fn
CC_4CELL_QUQX
CC_4_BETA_BUMP_0
CC_4_BETA_BUMP_EXPLICIT
CC_4_PROPS
CC_CARD2
CC_CARD_LESS_THAN_5
CC_CELL3
CC_CELL34
CC_CELL4
CC_CELL_CONVEX_HULL_INJ
CC_CELL_EXTREME_CARD
CC_CELL_INDEPENDENT
CC_CELL_IN_MCELL_SET
CC_CELL_NOT_COPLANAR
CC_CELL_NOT_COPLANAR_EXTREME
CC_CELL_NOT_NULLSET
CC_CELL_SUBSET_WEDGE
CC_CELL_WEDGE_MATCH_UH
CC_EXISTS
CC_KE_34
CC_PE_FACET_OF
CC_QU_SMALL_SITUATION
CDEUSDF
CDTETAT
CDTETAT_lemma1
CELL3_NONDEG
CELL4_NONDEG
CELL_CLUSTER_ESTIMATE_PROPS
CELL_CLUSTER_ESTIMATE_REDUCE
CELL_CLUSTER_N_LE_1
CELL_DOMAIN_IMP_INTERVAL_ARITH
CELL_LIST_PASS_ACC_INTRO
CELL_LIST_PASS_ACC_REV
CELL_LIST_PASS_MOVE1
CELL_LIST_PASS_MOVE2
CELL_LIST_PASS_NIL1
CELL_LIST_PASS_NIL2
CELL_LIST_PASS_SAME_HD
CELL_NN
CELL_PASS_GLUE
CELL_PASS_IMP
CENTER_IN_VORONOI_CELL
CENTRE_IN_BALL
CENTRE_IN_CBALL_FAN
CFFONNL
CFYXFTY0
CFYXFTY1
CHANGE_A_SCS_MOD
CHANGE_A_SCS_MODL
CHANGE_A_SCS_MODR
CHANGE_B_SCS_MOD
CHANGE_B_SCS_MODL
CHANGE_B_SCS_MODR
CHANGE_SIDE
CHANGE_SUM_TAU_FUN
CHANGE_TARJJUW_1
CHANGE_TARJJUW_10
CHANGE_TARJJUW_11
CHANGE_TARJJUW_12
CHANGE_TARJJUW_2
CHANGE_TARJJUW_3
CHANGE_TARJJUW_31
CHANGE_TARJJUW_32
CHANGE_TARJJUW_4
CHANGE_TARJJUW_5
CHANGE_TARJJUW_6
CHANGE_TARJJUW_7
CHANGE_TARJJUW_71
CHANGE_TARJJUW_8
CHANGE_TARJJUW_9
CHANGE_W_IN_BBS_MOD_IS_SCS
CHANGE_W_IN_BBS_MOD_LE3
CHANG_BIET_GI
CHI_MSB_ADDITIVE
CHI_MSB_AFF_GT_0
CHI_MSB_CONVEX
CHI_MSB_COPLANAR
CHI_MSB_IMP_COPLANAR
CHI_MSB_INCLUDES_CONVEX_HULL
CHI_MSB_POS2
CHOICE_CONST_LEMMA
CHOOSE_MOD_3
CIRCLE_SINCOS_PI
CIRCULAR_SOL_EQ_2PI
CIRCUMCENTER_1
CIRCUMCENTER_2
CIRCUMCENTER_FORMULAR
CIRCUMCENTER_FORMULAR2
CIRCUMCENTER_IN_VORONOI_SET
CIRCUMCENTER_LEMMA
CIRCUMCENTER_NOT_EQ
CIRCUMCENTER_PROPTIES
CIRCUMCENTER_TRANSLATION
CIRCUMCENTER_lemma
CIZMRRH
CJBDXXN
CKQOWSA
CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1
CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2
CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
CLOSED_APPROACHABLE_FAN
CLOSED_BALL_ANNULUS
CLOSED_BIS_LE
CLOSED_CBALL_FAN
CLOSED_CLOSURE_FAN
CLOSED_CONDITION1_SY
CLOSED_CONVEX_HULL_FINITE
CLOSED_DIFF_FAN
CLOSED_DISCRETE
CLOSED_EMPTY_FAN
CLOSED_HALFSPACE_GE_FAN
CLOSED_HALFSPACE_LE_FAN
CLOSED_HYPERPLANE_FAN
CLOSED_INTERS_FAN
CLOSED_INTERVAL_LEFT_FAN
CLOSED_INTERVAL_RIGHT_FAN
CLOSED_INTER_COMPACT_FAN
CLOSED_INTER_FAN
CLOSED_IN_CLOSED_FAN
CLOSED_IN_CLOSED_TRANS_FAN
CLOSED_IN_DIFF
CLOSED_IN_EMPTY
CLOSED_IN_FAN
CLOSED_IN_INTER
CLOSED_IN_INTERS
CLOSED_IN_REFL
CLOSED_IN_SUBSET
CLOSED_IN_TRANS_FAN
CLOSED_IN_UNION
CLOSED_LIFT_FAN
CLOSED_LIMPT_FAN
CLOSED_MATVEC
CLOSED_MCELL
CLOSED_MULTIPLES_FAN
CLOSED_NEGATIONS_FAN
CLOSED_PASTECART_FAN
CLOSED_POSITIVE_ORTHANT_FAN
CLOSED_RCONE_GE
CLOSED_ROGERS
CLOSED_SEQUENTIAL_LIMITS_FAN
CLOSED_SET_OF_LIST_KY_LEMMA_1
CLOSED_SET_OF_LIST_KY_LEMMA_2
CLOSED_SING_FAN
CLOSED_SY
CLOSED_TRI_SY
CLOSED_UNIONS_FAN
CLOSED_UNION_FAN
CLOSED_UNIV_FAN
CLOSED_VORONOI_CLOSED
CLOSED_VORONOI_LIST
CLOSED_WEDGE
CLOSED_WEDGE_EQ_PI
CLOSED_WEDGE_LT_PI
CLOSEST_POINT_SING
CLOSEST_POINT_SUBSET_lemma
CLOSURE_AFF_GT_1_3_EQ_AFF_GE_1_3
CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1
CLOSURE_APPROACHABLE_FAN
CLOSURE_BALL_FAN
CLOSURE_BIS_LT
CLOSURE_CLOSED_FAN
CLOSURE_CLOSURE_FAN
CLOSURE_EQ_FAN
CLOSURE_HULL_FAN
CLOSURE_INTERIOR_FAN
CLOSURE_MINIMAL_FAN
CLOSURE_SEQUENTIAL_FAN
CLOSURE_SUBSET_FAN
CLOSURE_UNIQUE_FAN
CLOSURE_VORONOI_OPEN
CNICGSF1
CNICGSF2
CNICGSF3
CNICGSF4
CNICGSF5
CNVX_IMP_INTERIOR_ANGLE_PI
COEF1_NEG_IFF_V1_IN_AFF_LT
COEF1_POS_EQ_V1_IN
COEFS
COEFS1_EQ_0_IFF_V_IN_AFF
COEFS_4
COEF_1_EQ_ZERO
COEF_1_POS_NEG
COFACTOR_COLUMN
COFACTOR_MATRIX_INV
COFACTOR_ROW
COFACTOR_TRANSP
COLLINEAR2
COLLINEAR_1
COLLINEAR_2
COLLINEAR_3
COLLINEAR_3_2D
COLLINEAR_3_DOT_MULTIPLES
COLLINEAR_3_EXPAND
COLLINEAR_3_TRANS
COLLINEAR_4_3
COLLINEAR_AZIM_0_OR_PI
COLLINEAR_AZIM_CYCLE_B_SY
COLLINEAR_BETWEEN_CASES
COLLINEAR_B_SY
COLLINEAR_CROSS_0
COLLINEAR_DISJOINT3
COLLINEAR_DISJOINT_PERM3
COLLINEAR_DIST_BETWEEN
COLLINEAR_EMPTY
COLLINEAR_EQ_SUB
COLLINEAR_EQ_SUB_NEG
COLLINEAR_EX
COLLINEAR_IMP_COPLANAR
COLLINEAR_IMP_POS_UPS2
COLLINEAR_LEMMA
COLLINEAR_LEMMA_ALT
COLLINEAR_LINEAR_IMAGE
COLLINEAR_LINEAR_IMAGE_EQ
COLLINEAR_MIDPOINT
COLLINEAR_NORM_LT_0
COLLINEAR_ONCE_VEC_0
COLLINEAR_ORTHO_PLANE
COLLINEAR_POINT_SYM_0
COLLINEAR_SING
COLLINEAR_SIN_ARCV_0
COLLINEAR_SMALL
COLLINEAR_SUBSET
COLLINEAR_SUBSET_AFF2
COLLINEAR_SYM_0
COLLINEAR_TRANSABLE
COLLINEAR_TRANSLATION
COLLINEAR_TRANSLATION_EQ
COLLINEAR_TRIPLES
COLLINEAR_UNEQUAL
COLLINEAR_WITHIN_AFF_GE_COLLINEAR
COLLINERA_AS_IN_CONV2
COLL_AFF_GT_2_1
COLL_EQ_DEPENDENT
COLL_IFF_COLL_CROSS
COLL_IFF_COLL_CROSS2
COLL_IN_AFF_GT_AFF_GT_EQ
COLL_IN_AFF_GT_INTER_EMPTY
COLL_IN_AFF_GT_TOO
COLUMNS_IMAGE_BASIS
COLUMNS_TRANSP
COLUMN_TRANSP
COL_EQ_NORM_CROSS
COMMUTATIVE_POINT_PAIR_0
COMM_BIJ_HAS_SAME_ORDS
COMM_INVERSE_LEMMA
COMM_ORBIT_IMAGE_LEMMA
COMM_ORBIT_IMAGE_LEMMA_PERMUTES
COMM_POWER_LEMMA
COMM_POWER_LEMMA_PERMUTES
COMM_RES_INVERSE_LEMMA
COMM_RES_INVERSE_LEMMA'
COMPACT_AFFINITY_FAN
COMPACT_ATTAINS_INF_FAN
COMPACT_ATTAINS_SUP_FAN
COMPACT_BALL_ANNULUS
COMPACT_BALL_ANNULUS_MATVEC
COMPACT_CBALL_FAN
COMPACT_CONTINUOUS_IMAGE_FAN
COMPACT_DIFFERENCES_FAN
COMPACT_EMPTY_FAN
COMPACT_EQ_BOLZANO_WEIERSTRASS_FAN
COMPACT_EQ_BOUNDED_CLOSED_FAN
COMPACT_EQ_HEINE_BOREL_FAN
COMPACT_FRONTIER_BOUNDED_FAN
COMPACT_FRONTIER_FAN
COMPACT_IMP_BOUNDED_FAN
COMPACT_IMP_CLOSED_FAN
COMPACT_IMP_COMPLETE_FAN
COMPACT_IMP_FIP_FAN
COMPACT_IMP_HEINE_BOREL_FAN
COMPACT_IMP_TOTALLY_BOUNDED_FAN
COMPACT_INTER_CLOSED_FAN
COMPACT_INTER_FAN
COMPACT_LEMMA_FAN
COMPACT_MATVEC
COMPACT_MULTIPLES_FAN
COMPACT_NEGATIONS_FAN
COMPACT_PASTECART_FAN
COMPACT_REAL_LEMMA_FAN
COMPACT_SING_FAN
COMPACT_SPHERE_0
COMPACT_SUMS_FAN
COMPACT_SUP_MAXDISTANCE_FAN
COMPACT_TRANSLATION_FAN
COMPACT_TRI_STABLE
COMPACT_UNIFORMLY_CONTINUOUS_FAN
COMPACT_UNION_FAN
COMPACT_VORONOI_CLOSED
COMPATIBLE_BW_TWO_LEMMAS
COMPATIBLE_BW_TWO_LEMMAS2
COMPATIBLE_BW_TWO_LEMMAS2_ALT
COMPLEMENT_SET_FAN
COMPLETE_EQ_CLOSED_FAN
COMPLETE_UNIV_FAN
COMPONENTS_3
COMPONENTS_HYPERMAP_OF_FAN
COMPONENTS_HYPERMAP_OF_LIST
COMPONENTS_ISO_IMAGE
COMPONENT_LE_INFNORM
COMPONENT_LE_NORM
COMPONENT_LE_NORM_3
COMPOSE_BIJ
COMPOSE_INJ
COMPOSE_SURJ
COMPUTE_DELTA_OVER
COMPUTE_DELTA_X
COMPUTE_DELTA_X_AFTER_RESCALE
COMPUTE_DERIVATIVE_ONE
COMPUTE_DERIVATIVE_TWO
COMPUTE_DIHV_ATN2
COMPUTE_EULER_P_AFTER_RESCALE
COMPUTE_NORM_OF_P
COMPUTE_NORM_POW2
COMPUTE_SIN_DIVH_POW2
COMPUTE_TO_QUA_POLY
COMP_ASSOC
COMP_BIJ
COMP_INJ
COMP_SURJ
COM_POWER
COM_POWER_FUNCTION
CON3_SUB_CONE3
CONDITION1_SY
CONDITION2_SY
CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
CONDITION_DART_IN_NODE
CONDITION_INANGLE_CROSS_DOT
CONDS_FOR_INTER_AFF_CONV0
CONDS_IN_CONV2
CONDS_IN_HAFL_LINE
CONDS_IN_V_PRIME_NUM
CONDS_IN_V_PRIME_NUM2
CONDTION_A_LT_B
COND_COMPONENT
COND_FALSE
COND_FOR_CIRCUMCENTER_PROPERTIESS
COND_FOR_EXISTS_ANY_PERI
COND_MUL
COND_Q_SYS
CONE0_AFF_GT
CONE0_FCHANGED
CONE0_FCHANGED_AFF_GT
CONE0_FCHANGED_SCALE
CONE0_RELATIVE_INTERIOR_FACET
CONE0_SCALE
CONE0_SUBSET_WEDGE
CONIC_AFF_GE_0
CONIC_CAP_AFF_GT_EQ_0
CONIC_CAP_INTER_CONVEX_HULL_4_GT_0
CONIC_CAP_WEDGE_EQ_0
CONNECTED_CLOPEN_FAN
CONNECTED_COMPONENT_OF_SUBSET
CONNECTED_COMPONENT_TRANS
CONNECTED_CONTINUOUS_IMAGE_FAN
CONNECTED_EMPTY_FAN
CONNECTED_FCHANGED
CONNECTED_HALF_LINE
CONNECTED_HALF_LINE1
CONNECTED_REAL_LEMMA
CONNECTED_RELATIVE_INTERIOR_FACET
CONNECTED_SEGMENT_NOT_COVERED
CONSI_OF_LE77
CONSTANCE_FUN_CONTINUOUS
CONST_INTERVAL
CONS_IMP_CONTINUOUS_ATREAL
CONS_IMP_SO_IVS
CONS_LINEAR_IMAGE
CONS_TRANSLATION
CONTAINS_BALL_AFFINE_HULL
CONTINOUS_OPEN_PREIMAGE_FAN
CONTINUOUS_ADD_FAN
CONTINUOUS_ATREAL_DISTINCT
CONTINUOUS_ATREAL_DISTINCT_FINITE
CONTINUOUS_ATREAL_INJ_PRESERVED
CONTINUOUS_ATREAL_SQRT_COMPOSE
CONTINUOUS_ATTAINS_INF_FAN
CONTINUOUS_ATTAINS_SUP_FAN
CONTINUOUS_AT_COMPOSE_FAN
CONTINUOUS_AT_FAN
CONTINUOUS_AT_ID_FAN
CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN
CONTINUOUS_AT_IMP_CONTINUOUS_WITHIN_FAN
CONTINUOUS_AT_INV_FAN
CONTINUOUS_AT_LIFT_COMPONENT_FAN
CONTINUOUS_AT_LIFT_DOT_FAN
CONTINUOUS_AT_LIFT_NORM_FAN
CONTINUOUS_AT_LIFT_RANGE_FAN
CONTINUOUS_AT_OPEN_FAN
CONTINUOUS_AT_SEQUENTIALLY_FAN
CONTINUOUS_AT_SQRT
CONTINUOUS_AT_SQRT_COMPOSE
CONTINUOUS_AT_WITHIN_INV_FAN
CONTINUOUS_CLOSED_PREIMAGE_CONSTANT
CONTINUOUS_CMUL_FAN
CONTINUOUS_CONST_FAN
CONTINUOUS_CONTINUOUS_ATREAL
CONTINUOUS_CONTINUOUS_WITHINREAL
CONTINUOUS_CROSS
CONTINUOUS_FUNS_DISTINCT_POINTS
CONTINUOUS_FUN_DISTINCT_FINITE_SET
CONTINUOUS_INV_FAN
CONTINUOUS_LIFT_COMPONENT
CONTINUOUS_LIFT_DOT2
CONTINUOUS_MK_SIMPLEX_WITHINREAL
CONTINUOUS_NEG_FAN
CONTINUOUS_ON_ADD_FAN
CONTINUOUS_ON_CLOSED_FAN
CONTINUOUS_ON_CMUL_FAN
CONTINUOUS_ON_COMPOSE_FAN
CONTINUOUS_ON_CONST_FAN
CONTINUOUS_ON_CROSS
CONTINUOUS_ON_DET
CONTINUOUS_ON_D_FUN
CONTINUOUS_ON_D_FUN3
CONTINUOUS_ON_EQ_CONTINUOUS_AT_FAN
CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN
CONTINUOUS_ON_FAN
CONTINUOUS_ON_ID_FAN
CONTINUOUS_ON_INTERIOR_FAN
CONTINUOUS_ON_INVERSE_FAN
CONTINUOUS_ON_LIFT_COMPONENT_FAN
CONTINUOUS_ON_LIFT_DOT
CONTINUOUS_ON_LIFT_DOT2
CONTINUOUS_ON_LIFT_DOT_FAN
CONTINUOUS_ON_LIFT_NORM_FAN
CONTINUOUS_ON_LIFT_PRODUCT
CONTINUOUS_ON_LIFT_RANGE_FAN
CONTINUOUS_ON_NEG_FAN
CONTINUOUS_ON_OPEN_FAN
CONTINUOUS_ON_RHO_FUN_AND_AZIM
CONTINUOUS_ON_ROW
CONTINUOUS_ON_SAME_DOMAIN
CONTINUOUS_ON_SEQUENTIALLY_FAN
CONTINUOUS_ON_SUBSET_FAN
CONTINUOUS_ON_SUB_FAN
CONTINUOUS_ON_TAU_FUN
CONTINUOUS_ON_TAU_STAR
CONTINUOUS_POS_PRES
CONTINUOUS_PRESERVE_COLLINEAR
CONTINUOUS_SUB_FAN
CONTINUOUS_WITHINREAL_SQRT_COMPOSE
CONTINUOUS_WITHIN_COMPOSE_FAN
CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE
CONTINUOUS_WITHIN_FAN
CONTINUOUS_WITHIN_ID_FAN
CONTINUOUS_WITHIN_SEQUENTIALLY_FAN
CONTINUOUS_WITHIN_SQRT_COMPOSE
CONTINUOUS_WITHIN_SUBSET_FAN
CONTRAVENING_AZIM_DART_EQ_DIH_Y
CONTRAVENING_DART_DIST
CONTRAVENING_DIST
CONTRAVENING_ESTD_DIST
CONTRAVENING_FAN
CONTRAVENING_HAS_SIZE_lemma
CONTRAVENING_IMP_AZIM_DART_EQ_AZIM
CONTRAVENING_IMP_CARD_FACE_GE_3
CONTRAVENING_IMP_DART_FST_NEQ_SND
CONTRAVENING_IMP_FULLY_SURROUNDED
CONTRAVENING_IMP_IN_DART1_OF_FAN
CONTRAVENING_IMP_NOT_COPLANAR
CONTRAVENING_IMP_SURROUNDED
CONTRAVENING_LMFUN_BOUND
CONTRAVENING_TAUVEF_EQ_TAUM
CONTRAVENING_TRIANGULAR_FACE_DIST
CONTS_FUN_CONTINUOUS_ATREAL
CONT_ATREAL_INJ_PRESERVED
CONT_ATREAL_REAL_CONTS
CONV02_SUBSET_AFF2
CONV02_SU_CONV2
CONV0_4
CONV0_AFF_GT_EQ
CONV0_SET2
CONV0_SING
CONV0_SUBSET_AFF_GT
CONV0_SUB_CONV
CONV2_CONV3
CONV3_A_EQ
CONV3_CONV2
CONV3_EQ
CONV3_SUBSET_AFF_GE_3S
CONVERGENT_BOUNDED_INCREASING_FAN
CONVERGENT_BOUNDED_MONOTONE_FAN
CONVERGENT_EQ_CAUCHY_FAN
CONVERGENT_IMP_CAUCHY_FAN
CONVEX_AS_CONV2
CONVEX_BIS
CONVEX_BIS_LE
CONVEX_CLOSURE_DARTSET_LEADS_INTO_FAN
CONVEX_CLOSURE_FCHANGED
CONVEX_HULL_4
CONVEX_HULL_4_AFF_GE
CONVEX_HULL_4_EQUIV
CONVEX_HULL_4_IMP_2_2
CONVEX_HULL_4_IMP_3_1
CONVEX_HULL_4_SUBSET_AFF_GE_2_2
CONVEX_HULL_BREAK_KY_LEMMA
CONVEX_HULL_EQ_EQ_SET_EQ
CONVEX_HULL_KY_LEMMA_5
CONVEX_HULL_SCALE
CONVEX_HULL_SUBSET
CONVEX_IM_CONV02_SU
CONVEX_IM_CONV2_SU
CONVEX_LOCAL_FAN_SYM_0
CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
CONVEX_LOFA_IMP_INANGLE_LE_PI
CONVEX_OPEN_AFF_GT_FACE
CONVEX_PLANE_INTER
CONVEX_R3_INTER
CONVEX_RCONE_GE
CONVEX_RCONE_GT
CONVEX_RELATIVE_INTERIOR
CONVEX_RELATIVE_INTERIOR_FACE
CONVEX_RELATIVE_INTERIOR_FACET
CONVEX_SOME_WEDGE
CONVEX_VORONOI_CLOSED
CONVEX_VORONOI_LIST
CONVEX_WEDGE_LE_PI
CONV_BAR_EQ
CONV_CONV0
CONV_CONVEX_HULL
CONV_EM
CONV_MONO
CONV_SET2
CONV_SET3
CONV_SING
CONV_SUBSET_AFF_GE
CONV_UNION_SUB_AFF_GE
CONV_UNION_lemma
CON_ATREAL_REAL_CON
CON_ATREAL_REAL_CON2
CON_ATREAL_REAL_CON2_REDO
COPLANAR
COPLANAR_3
COPLANAR_AFF_GE_REDUCE
COPLANAR_AFF_GE_REDUCE2
COPLANAR_ALT
COPLANAR_AZIM_EQ
COPLANAR_CONVEX_HULL_COPLANAR
COPLANAR_DET_EQ_0
COPLANAR_DET_VEC3_EQ_0
COPLANAR_IFF_CROSS_DOT
COPLANAR_IMP_AFF_DIM
COPLANAR_IMP_DIH_PI
COPLANAR_INSERT
COPLANAR_UNION
COSG
COS_ARCV
COS_ARCV_EQ_ARCV
COS_ARG_VECTOR_ANGLE
COS_DERIVATIVES
COS_EQ_NEG_SIN
COS_MONOPOLY
COS_MONOPOLY_EQ
COS_NEGPOS_PI
COS_PERIODIC_IN_WHOLE
COS_PERIODIC_N2PI
COS_PI3
COS_PI6
COS_POW2_INTER
COS_SUM_2PI
COS_TOTAL
COS_TREBLE_COS
COUNTABLE_CARD
COUNTABLE_IMAGE
COUNTABLE_NUMSEG
COUNTABLE_UNIONS
COVER1_SY
COVER2_SY
COVER3_SY
COVER4_SY
COVER5_SY
COVER6_SY
COVER_NOT_EAR_SY
COVER_SY
COVEX_OF_LOFA_HALF_CIRCLE
COVEX_OF_LOFA_HALF_CIRCLE2
CQAOQLR
CRAMER
CRAMER_LEMMA
CRAMER_LEMMA1
CRAMER_LEMMA_TRANSP
CRAMER_MATRIX_LEFT
CRAMER_MATRIX_LEFT_INVERSE
CRAMER_MATRIX_RIGHT
CRAMER_MATRIX_RIGHT_INVERSE
CRAZY_THMMM
CRITICAL_EDGEX_ALT
CRITICAL_EDGEX_BOUND
CRITICAL_EDGEX_SUBSET_MCELL
CRITICAL_WEIGHT_POS_LE
CROSS_CONVERT
CROSS_DOT_COPLANAR
CROSS_DOT_POS_SY
CROSS_DOT_SEQUENTIALLY
CROSS_IN_SAME_DIRECTION
CROSS_LAGRANGE1
CROSS_LSUB
CROSS_LZERO
CROSS_PAIR_NOT_IN_FF
CROSS_POSITIVE_MULTIPLE_AZIM_AXIS
CROSS_POSITIVE_MULTIPLE_AZIM_AXIS_ALT
CROSS_RSUB
CROSS_RZERO
CROSS_SQUARED
CRTTXAT
CRTTXAT_lemma1
CRTTXAT_lemma1'
CRTTXAT_lemma2
CS_ADJ
CTVTAQA
CUXVZOZ
CVLF_COLLINEAR_CIRCULAR_LUNAR
CVLF_FLAT_ANGLE_LEMMA
CVLF_LF_F
CVX_LO_IMP_LO
CYCLIC_MAP_IMP_CIRCLE_ITSELF
CYCLIC_SET
CYCLIC_SET_EDGE_FAN
CYCLIC_SET_IMP_NOT_COLLINEAR
CYCLIC_SET_IMP_SELF_LOPP2
CYCLIC_SET_IMP_SELF_LOPP3
CYCLIC_SET_IMP_STABLE_SET2
CYCLIC_SET_LINEAR_IMAGE
CYCLIC_SET_TRANSLATION_EQ
CYLINDER_CORDINATE
C_COEF_FORMULA
C_LE_2_IS_SCS
C_LT_2_IS_SCS
c2001
c3_lemma
c_4_azim_mcell_dih_y
c_cone
c_def38
c_inv_nov18
c_nov16
c_nov17
c_nov18
c_nov18e
c_nov18e1
c_nov18e2
c_nov18e3
c_nov1_17
c_union
cancel
canon
canon_darts
canon_flag
canon_loop
card_diff_ineq
card_ds2_fanadd_eq3
card_eq_ball_point
card_eq_image_in_d_fan
card_int_ball_ineq
card_int_ball_le
card_int_ball_le2
card_int_ball_pos
card_nfan_neq0
card_node
card_orb_neq0
card_orbit_le
card_packing_annulus
card_packing_ball
card_partition_formula
case2_proof_fan
cat
cat_empty'
catrev
cauchy_fan
cauchy_ineq
cautruc1
cautruc10
cautruc11
cautruc2
cautruc3
cautruc4
cautruc5
cautruc6
cautruc7
cautruc8
cautruc9
cayleyR
cayleyR_quadratic
cayleytr
cball_fan
cc_4
cc_4_UL
cc_4_cc_cell
cc_4_cc_ke4
cc_4cell_v11
cc_A0
cc_azim_v11
cc_bool_data
cc_bool_model_data
cc_bool_model_simple
cc_bool_model_simple2
cc_bool_model_v11
cc_bool_prep_v11
cc_bool_v11
cc_card_data
cc_card_v11
cc_cell
cc_crit_v11
cc_cut_sum
cc_data_v8
cc_eps
cc_gg3a_v11
cc_gg3b_v11
cc_gg_v11
cc_hassmall_v11
cc_ke
cc_pe
cc_pe_exists
cc_prep_model_data
cc_qu_v11
cc_qx_v11
cc_qy_v11
cc_real_dat_def
cc_real_data
cc_real_model_data
cc_real_model_simple
cc_real_model_v11
cc_real_v11
cc_size_v11
cc_small_eta_v11
cc_small_v11
cc_subcrit_v11
cc_supercrit_v11
cc_uh
cc_uh_exists
ccube
ccube_eq_interval
ccube_to_ball
cell3_008_from_ineq_ALT
cell3_008_from_ineq_thm
cell3_from_ineq_thm
cell3_from_ineq_thm_ALT
cell_3_delta_x_eta_x
cell_cluster
cell_cluster_estimate_A
cell_cluster_estimate_v1
cell_domain
cell_params
cell_params_d
cell_pass
center_pac
centered_pac
ch_le
cha_lemma1
change_parameters
change_spherical_coordinate_fan
change_to_margin
change_type_v2
change_type_v3
chi
chi_msb
chi_msb_additive_a
chi_msb_additive_d
chi_msb_swap_01
chi_msb_swap_12
chi_msb_swap_23
chi_rad2
chi_x
choice_and_head_tail
choice_at_margin
choice_identity
choice_reflect
choose_nd_point
chop0
chop1
chop2
chop3
chop4
chop5
circular
circular_cone
circumcenter
circumradius
ckq_in_ball_annulus
close_hinhcau
closed_aff_ge_1_2
closed_aff_ge_2_1
closed_aff_ge_ballnorm_fan
closed_ballnorm_fan
closed_fan
closed_half_plane
closed_half_space
closed_halfline_fan
closed_in
closed_interval_fan
closed_point_fan
closure_fan
cluster_gamma_AX
cluster_gamma_v1
cm3_ups_x
cofactor
collinear
collinear1_continuous_fan
collinear1_fan
collinear_continuous_fan
collinear_cross
collinear_expand
collinear_fan
collinear_imp_azim_is_rezo_fan
collinear_translate_axis
collinears_fan
column
columns
columnvector
comb_component
comb_trans
combinator_lemma
commutative
compact_aff_ge_ballnorm_fan
compact_fan
compact_imp_fip_fan
compare_left
compare_right
complement
complement_index
complement_set
complete_fan
complex_frac_cancel
complex_taylor_catn
component_at_isolated_dart
component_hinhcau_bound
compose
compose6
compute_one_first
compute_one_second
compute_two_first
compute_two_second
concat
concatenate_contours
concatenate_paths
concatenate_two_contours
concatenate_two_disjoint_contours
concatenate_two_paths
condA
condC
condF
condS
condition1_to_in_aff_gt_by_angle
condition_4point_aff_gt_1_2inter_aff_gt_1_2
condition_aff_gt_subset_yfan
condition_azim_imp_edge_fan
condition_azim_le_pi
condition_cross_dot_4point
condition_edge_in_face_fan
condition_f1_eq_fan
condition_f1_fan_in_face_set
condition_f1_fan_power_in_face_set
condition_hypermap_fan
condition_not_edge_fan
condition_not_intersection_fan
condition_not_intersection_point_fan
condition_rw_dart_fan_inter_aff_gt_is_not_empty
condition_set_of_edge_eq_empty
condition_to_in_aff_gt_by_angle
condition_unique_by_dart_leads_into
conditions_in_rcone_fan
cone
cone0
cone0_subset_lune
cone_ge_fan
cone_ge_fan_inter_aff_ge_is_empty
cone_ge_fan_inter_aff_ge_is_empty_fan
conflict_diagonal
conflicting_dia
conforming
conforming_bijection
conforming_bijection_fan
conforming_bijection_fanadd
conforming_bijection_fanadd_verrion
conforming_diagonal
conforming_diagonal_fan
conforming_diagonal_fan_ds_fanadd
conforming_diagonal_fanadd1
conforming_fan
conforming_half_space
conforming_half_space_fan
conforming_solid_angle
conforming_solid_angle_fan
conic_cap
conjg
connect_insidepoint_to_bound_yfan
connected_component_of_faces_fan
connected_dart_leads_into_fan
connected_fan
connected_hypermap
connected_in_dartset_leads_into_fan_union_aff_gt
connected_rw_dart_fan
const1
const1'
const1_pos
constant
constant6
constraint_system
context
continuous_at_fan
continuous_change_spherical_coordinate_fan
continuous_coplanar_fan
continuous_fan
continuous_intersection_point
continuous_lemma_aff_ge
continuous_lemma_dec
continuous_lemma_inc
continuous_nbd_pos
continuous_on_fan
continuous_preimage_closed
continuous_preimage_open
continuous_set_fan
continuous_solution_aux
continuous_within_fan
continuum_bij
continuum_family
contracted_dart
contravening
contravening_imp_conforming
conv
conv0
conv0_2
conv0pt
conv1pt
conv_trg
convex
convex3
convex3_in_inters
convex_local_fan
convex_local_fan_azim_le_pi
convex_nua_kg
convex_sum_corollary
convex_voronoi
convolution_belong
convolution_inv
convolution_rep
coord3
coordinates_lemma
coplanar
coplanar_aff_gt_simple
coplanar_alt
coplanar_cross_dot
coplanar_cross_reduction
coplanar_cross_scale
coplanar_delta_y
coplanar_delta_y_zero
coplanar_eq_coplanar_alt
coplanar_imp_continuous_collinear
coplanar_in_affine_hull
coplanar_is_cross_fan
cos797
cosV
cos_2nz
cos_acs_pi6
cos_arc
cos_bounds_0_Pi2
cos_bounds_0_pi
cos_nz
cos_of_u_fan
coset
cosets
cotext
count
countable_bij
countable_s
critical_edgeX
critical_edgeX_critical_edge_y
critical_edge_bound
critical_edge_subset_mcell
critical_edge_y
critical_weight
critical_weight1
critical_weight1a
critical_weight1b
critical_weight_wtcount6_y
critical_y_range
cross
cross_dot_fully_surrounded1_fan
cross_dot_fully_surrounded1_fan_le
cross_dot_fully_surrounded2_fan
cross_dot_fully_surrounded2_fan_le
cross_dot_fully_surrounded_fan
cross_dot_fully_surrounded_ge_fan
cross_independent
cross_mag
cross_skew
cross_triple
cs_adj
cs_adj4_EXPLICIT
cs_adj_SUC
cstab
cth0
cube
cube_eq_interval
cube_to_ball
cut_aff_gt_1_3_connected
cut_in_angle_fan
cut_in_edges_fan
cut_inside_fan
cw_dart_fan
cw_node_fan
cwedge
cycle
cyclic_hypermap
cyclic_inverses_maps
cyclic_maps
cyclic_on
cyclic_power_sigma_fan
cyclic_set
cyclic_set_scale