HOL html

Files Index

Theorems Index

I (theorems)

ICOSAHEDRON_CONGRUENT_EDGES
ICOSAHEDRON_CONGRUENT_FACETS
ICOSAHEDRON_EDGES
ICOSAHEDRON_EDGES_PER_FACE
ICOSAHEDRON_EDGES_PER_VERTEX
ICOSAHEDRON_VERTICES
IDEMPOTENT_IMP_RETRACTION
ID_INT
ID_PAR
ID_SEQ
IF
IF1_SEQ
IF2_SEQ
IF_PAR
II_NZ
IM
IMAGE
IMAGE2
IMAGE_AFFINITY_INTERVAL
IMAGE_AFFINITY_REAL_INTERVAL
IMAGE_CLAUSES
IMAGE_CLOSURE_SUBSET
IMAGE_COMPOSE_PERMUTATIONS_L
IMAGE_COMPOSE_PERMUTATIONS_R
IMAGE_CONST
IMAGE_CX
IMAGE_DELETE_INJ
IMAGE_DIFF_INJ
IMAGE_DROPOUT_CLOSED_INTERVAL
IMAGE_DROP_INTERVAL
IMAGE_DROP_UNIV
IMAGE_EQ_EMPTY
IMAGE_EQ_NTRIE_IMAGE
IMAGE_FSTCART_PCROSS
IMAGE_I
IMAGE_ID
IMAGE_IMP_INJECTIVE
IMAGE_IMP_INJECTIVE_GEN
IMAGE_INJECTIVE_IMAGE_OF_SUBSET
IMAGE_INTERS
IMAGE_INTER_INJ
IMAGE_INVERSE_PERMUTATIONS
IMAGE_LEMMA_0
IMAGE_LEMMA_1
IMAGE_LEMMA_2
IMAGE_LIFT_DROP
IMAGE_LIFT_REAL_INTERVAL
IMAGE_LIFT_REAL_SEGMENT
IMAGE_LIFT_UNIV
IMAGE_SNDCART_PCROSS
IMAGE_STRETCH_INTERVAL
IMAGE_STRETCH_REAL_INTERVAL
IMAGE_SUBSET
IMAGE_SURJ
IMAGE_TWIZZLE_INTERVAL
IMAGE_UNION
IMAGE_UNIONS
IMAGE_WOP_LEMMA
IMAGE_o
IMP
IMPLIES
IMPLY_OR_lemma
IMPLY_WEAK_AND_lemma
IMPLY_WEAK_OR_lemma
IMPLY_WEAK_lemma
IMPLY_WEAK_lemma1
IMPLY_WEAK_lemma2
IMPLY_WEAK_lemma3
IMPLY_WEAK_lemma4
IMPLY_WEAK_lemma5
IMPLY_WEAK_lemma6
IMPLY_WEAK_lemma7
IMPLY_WEAK_lemma_b
IMPOSSIBILITY_B
IMP_CLAUSES
IMP_CONJ
IMP_CONJ_ALT
IMP_EQ_CLAUSE
IMP_EQ_EQ_EQ_NOT_OR
IMP_EQ_EQ_EQ_OR_NOT
IMP_EQ_OR_EQ_EQ_OR_NOT_OR
IMP_F_EQ_F
IMP_NOT_EQ_EQ_EQ_OR
IM_ADD
IM_CCOS
IM_CEXP
IM_CLOG_EQ_0
IM_CLOG_EQ_PI
IM_CLOG_POS_LE
IM_CLOG_POS_LT
IM_CLOG_POS_LT_IMP
IM_CMUL
IM_CNJ
IM_COMPLEX_DIV_EQ_0
IM_COMPLEX_DIV_GE_0
IM_COMPLEX_DIV_GT_0
IM_COMPLEX_DIV_LEMMA
IM_COMPLEX_DIV_LE_0
IM_COMPLEX_DIV_LT_0
IM_COMPLEX_INV_EQ_0
IM_COMPLEX_INV_GE_0
IM_COMPLEX_INV_GT_0
IM_COMPLEX_INV_LE_0
IM_COMPLEX_INV_LT_0
IM_CSIN
IM_CX
IM_DEF
IM_DIV_CX
IM_II
IM_LINEPATH_CX
IM_MUL_CX
IM_MUL_II
IM_NEG
IM_POW_2
IM_SUB
IM_VSUM
IN
INCLUSION_EXCLUSION
INCLUSION_EXCLUSION_MOBIUS
INCLUSION_EXCLUSION_REAL
INCLUSION_EXCLUSION_REAL_INDEXED
INCLUSION_EXCLUSION_REAL_RESTRICTED
INCLUSION_EXCLUSION_REAL_RESTRICTED_INDEXED
INCLUSION_EXCLUSION_SYMMETRIC
INCLUSION_EXCLUSION_USUAL
INCREASING_BOUNDED_REAL_VARIATION
INCREASING_BOUNDED_VARIATION
INCREASING_LEFT_LIMIT
INCREASING_LEFT_LIMIT_1
INCREASING_REAL_VARIATION
INCREASING_RIGHT_LIMIT
INCREASING_RIGHT_LIMIT_1
INCREASING_VECTOR_VARIATION
INDEFINITE_INTEGRAL_CONTINUOUS
INDEFINITE_INTEGRAL_CONTINUOUS_LEFT
INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT
INDEFINITE_INTEGRAL_UNIFORMLY_CONTINUOUS
INDEFINITE_INTEGRAL_UNIFORMLY_CONTINUOUS_EXPLICIT
INDEPENDENT_2
INDEPENDENT_3
INDEPENDENT_BOUND
INDEPENDENT_BOUND_GENERAL
INDEPENDENT_CARD_LE_DIM
INDEPENDENT_EMPTY
INDEPENDENT_EXPLICIT
INDEPENDENT_IMP_AFFINE_DEPENDENT_0
INDEPENDENT_IMP_FINITE
INDEPENDENT_INJECTIVE_IMAGE
INDEPENDENT_INJECTIVE_IMAGE_GEN
INDEPENDENT_INSERT
INDEPENDENT_LINEAR_IMAGE_EQ
INDEPENDENT_MONO
INDEPENDENT_NONZERO
INDEPENDENT_SING
INDEPENDENT_SPAN_BOUND
INDEPENDENT_STDBASIS
INDEX_0
INDEX_1
INDEX_DECOMPOSITION
INDEX_DECOMPOSITION_PRIME
INDEX_EQ_0
INDEX_EXP
INDEX_FACT
INDEX_FACT_ALT
INDEX_FACT_UNBOUNDED
INDEX_MUL
INDEX_ODDPART
INDEX_ODDPART_DECOMPOSITION
INDEX_ODDPART_UNIQUE
INDEX_ODDPART_WORK
INDEX_REFL
INDEX_TRIVIAL_BOUND
INDSET_IND_MODEL
INDSET_INHABITED
INDUCTION_FROM_1
INDUCTIVE_INVARIANT
INDUCT_COPRIME
INDUCT_COPRIME_STRONG
INDUCT_LINEAR_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY_ALT
INDUCT_MATRIX_ROW_OPERATIONS
INDUCT_SPECIAL
IND_EUCLID
IND_SUC_0_EXISTS
INESSENTIAL_EQ_CONTINUOUS_LOGARITHM
INESSENTIAL_EQ_CONTINUOUS_LOGARITHM_CIRCLE
INESSENTIAL_EQ_EXTENSIBLE
INESSENTIAL_IMP_CONTINUOUS_LOGARITHM_CIRCLE
INESSENTIAL_NEIGHBOURHOOD_EXTENSION_LOGARITHM
INESSENTIAL_ON_CLOPEN_UNIONS
INESSENTIAL_ON_COMPONENTS
INESSENTIAL_ON_COMPONENTS_EQ
INESSENTIAL_SPHEREMAP_2
INESSENTIAL_SPHEREMAP_LOWDIM
INESSENTIAL_SPHEREMAP_LOWDIM_GEN
INF
INFERISIGN_NEG_NEG_NEG
INFERISIGN_NEG_NEG_POS
INFERISIGN_NEG_POS_NEG
INFERISIGN_NEG_POS_POS
INFERISIGN_NEG_ZERO_NEG
INFERISIGN_NEG_ZERO_POS
INFERISIGN_POS_NEG_NEG
INFERISIGN_POS_NEG_POS
INFERISIGN_POS_POS_NEG
INFERISIGN_POS_POS_POS
INFERISIGN_POS_ZERO_NEG
INFERISIGN_POS_ZERO_POS
INFERISIGN_ZERO_NEG_NEG
INFERISIGN_ZERO_NEG_POS
INFERISIGN_ZERO_POS_NEG
INFERISIGN_ZERO_POS_POS
INFERISIGN_ZERO_ZERO_NEG
INFERISIGN_ZERO_ZERO_POS
INFERPSIGN_MATINSERT_THM
INFERPSIGN_NEG
INFERPSIGN_NEG_EVEN
INFERPSIGN_NEG_EVEN_LEM
INFERPSIGN_NEG_ODD_POS
INFERPSIGN_NEG_ODD_POS_LEM
INFERPSIGN_POS
INFERPSIGN_POS_EVEN
INFERPSIGN_POS_EVEN_LEM
INFERPSIGN_POS_ODD_POS
INFERPSIGN_POS_ODD_POS_LEM
INFERPSIGN_ZERO_EVEN
INFERPSIGN_ZERO_EVEN_LEM
INFERPSIGN_ZERO_ODD_POS
INFERPSIGN_ZERO_ODD_POS_LEM
INFINITE
INFINITE_ARC_IMAGE
INFINITE_CARD_LE
INFINITE_CHOOSE
INFINITE_DELETE
INFINITE_DIFF_FINITE
INFINITE_ENUMERATE
INFINITE_ENUMERATE_WEAK
INFINITE_FINITE_CHOICE
INFINITE_FROM
INFINITE_IMAGE_INJ
INFINITE_INSERT
INFINITE_INTEGER
INFINITE_MEMBER
INFINITE_NONEMPTY
INFINITE_OPEN_IN
INFINITE_PIGEONHOLE
INFINITE_RATIONAL
INFINITE_SIMPLE_PATH_IMAGE
INFINITE_SUPERSET
INFIN_HD_NEG_LEM
INFIN_HD_POS_LEM
INFIN_NEG_NEG
INFIN_NEG_POS
INFIN_NIL_NEG
INFIN_NIL_POS
INFIN_POS_NEG
INFIN_POS_POS
INFIN_SING_NEG_NEG
INFIN_SING_NEG_POS
INFIN_SING_POS_NEG
INFIN_SING_POS_POS
INFIN_TL_NEG_LEM
INFIN_TL_POS_LEM
INFNORM_0
INFNORM_2
INFNORM_EQ_0
INFNORM_EQ_1_2
INFNORM_EQ_1_IMP
INFNORM_LE_NORM
INFNORM_MUL
INFNORM_MUL_LEMMA
INFNORM_NEG
INFNORM_POS_LE
INFNORM_POS_LT
INFNORM_SET_IMAGE
INFNORM_SET_LEMMA
INFNORM_SUB
INFNORM_TRIANGLE
INFSUM_0
INFSUM_ADD
INFSUM_CMUL
INFSUM_EQ
INFSUM_LINEAR
INFSUM_NEG
INFSUM_RESTRICT
INFSUM_SUB
INFSUM_UNIQUE
INF_CLOSURE
INF_EQ
INF_FINITE
INF_FINITE_LEMMA
INF_INSERT
INF_INSERT_FINITE
INF_SING
INF_UNION
INF_UNIQUE
INF_UNIQUE_FINITE
INJ
INJA
INJA_INJ
INJECTIVE_ALT
INJECTIVE_EQ_1D_OPEN_MAP_UNIV
INJECTIVE_IFF_LEFT_INVERSE
INJECTIVE_IMAGE
INJECTIVE_IMP_ISOMETRIC
INJECTIVE_INTO_1D_EQ_HOMEOMORPHISM
INJECTIVE_INTO_1D_IMP_OPEN_MAP
INJECTIVE_INTO_1D_IMP_OPEN_MAP_UNIV
INJECTIVE_INVERSE
INJECTIVE_INVERSE_o
INJECTIVE_LEFT_INVERSE
INJECTIVE_LEFT_INVERSE_NONEMPTY
INJECTIVE_MAP
INJECTIVE_MAP_OPEN_IFF_CLOSED
INJECTIVE_ON_ALT
INJECTIVE_ON_IMAGE
INJECTIVE_ON_LEFT_INVERSE
INJECTIVE_PAD2D3D
INJECTIVE_SCALING
INJECTIVE_SURJECTIVE_PREIMAGE
INJF
INJF_INJ
INJN
INJN_INJ
INJP
INJP_INJ
INJ_IMAGE
INJ_INVERSE2
INJ_LEMMA
INJ_UNIV
INSEG_LINSEG
INSEG_PROPER_SUBSET
INSEG_PROPER_SUBSET_FL
INSEG_SUBSET
INSEG_SUBSET_FL
INSEG_WOSET
INSERT
INSERTAT
INSERTAT_0
INSERTAT_EL
INSERTAT_LENGTH
INSERTAT_TL
INSERT_AC
INSERT_COMM
INSERT_DEF
INSERT_DELETE
INSERT_DIFF
INSERT_INSERT
INSERT_INTER
INSERT_SUBSET
INSERT_UNION
INSERT_UNION_EQ
INSERT_UNIV
INSIDE_ABS
INSIDE_ARC_EMPTY
INSIDE_BOUNDED_COMPLEMENT_CONNECTED_EMPTY
INSIDE_COMPLEMENT_UNBOUNDED_CONNECTED_EMPTY
INSIDE_CONNECTED_COMPONENT_LE
INSIDE_CONNECTED_COMPONENT_LT
INSIDE_CONVEX
INSIDE_EMPTY
INSIDE_EQ_OUTSIDE
INSIDE_FRONTIER_EQ_INTERIOR
INSIDE_INSIDE
INSIDE_INSIDE_COMPACT_CONNECTED
INSIDE_INSIDE_EQ_EMPTY
INSIDE_INSIDE_SUBSET
INSIDE_INTER_OUTSIDE
INSIDE_IN_COMPONENTS
INSIDE_LBL
INSIDE_LINEAR_IMAGE
INSIDE_MONO
INSIDE_NO_OVERLAP
INSIDE_OF_TRIANGLE
INSIDE_OUTSIDE
INSIDE_OUTSIDE_INTERSECT_CONNECTED
INSIDE_OUTSIDE_UNIQUE
INSIDE_REL
INSIDE_SAME_COMPONENT
INSIDE_SIMPLE_CURVE_IMP_CLOSED
INSIDE_SUBSET
INSIDE_TRANSLATION
INSIDE_UNION_OUTSIDE
INSIDE_UNIQUE
INST_CORE
INST_CORE_EXISTS
INST_DEF
INST_TYPE_correct
INST_correct
INTEGER_ABS
INTEGER_ABS_MUL_EQ_1
INTEGER_ADD
INTEGER_ADD_EQ
INTEGER_CASES
INTEGER_CLOSED
INTEGER_DET
INTEGER_DIV
INTEGER_EXISTS_BETWEEN
INTEGER_EXISTS_BETWEEN_ABS
INTEGER_EXISTS_BETWEEN_ABS_LT
INTEGER_EXISTS_BETWEEN_ALT
INTEGER_EXISTS_BETWEEN_LT
INTEGER_MUL
INTEGER_NEG
INTEGER_POS
INTEGER_POW
INTEGER_PRODUCT
INTEGER_PSUM
INTEGER_ROUND
INTEGER_SIGN
INTEGER_SUB
INTEGER_SUB_EQ
INTEGER_SUB_LEMMA
INTEGER_SUM
INTEGER_WINDING_NUMBER
INTEGER_WINDING_NUMBER_EQ
INTEGRABLE_0
INTEGRABLE_ADD
INTEGRABLE_AFFINITY
INTEGRABLE_ALT
INTEGRABLE_ALT_SUBSET
INTEGRABLE_BOUNDED_VARIATION_PRODUCT
INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT
INTEGRABLE_BY_PARTS
INTEGRABLE_BY_PARTS_EQ
INTEGRABLE_CASES
INTEGRABLE_CAUCHY
INTEGRABLE_CCONTINUOUS_EXPLICIT
INTEGRABLE_CCONTINUOUS_EXPLICIT_SYMMETRIC
INTEGRABLE_CMUL
INTEGRABLE_CMUL_EQ
INTEGRABLE_COMBINE
INTEGRABLE_COMBINE_DIVISION
INTEGRABLE_COMPLEX_0
INTEGRABLE_COMPLEX_LMUL
INTEGRABLE_COMPLEX_LMUL_EQ
INTEGRABLE_COMPLEX_RMUL
INTEGRABLE_COMPLEX_RMUL_EQ
INTEGRABLE_COMPONENTWISE
INTEGRABLE_CONST
INTEGRABLE_CONTINUOUS
INTEGRABLE_DECREASING
INTEGRABLE_DECREASING_1
INTEGRABLE_DECREASING_PRODUCT
INTEGRABLE_DECREASING_PRODUCT_UNIV
INTEGRABLE_DEFINT
INTEGRABLE_EQ
INTEGRABLE_IFF_MEASURABLE_UNDER_CURVE
INTEGRABLE_IMP_MEASURABLE
INTEGRABLE_IMP_REAL_MEASURABLE
INTEGRABLE_INCREASING
INTEGRABLE_INCREASING_1
INTEGRABLE_INCREASING_PRODUCT
INTEGRABLE_INCREASING_PRODUCT_UNIV
INTEGRABLE_INTEGRAL
INTEGRABLE_LIMIT
INTEGRABLE_LINEAR
INTEGRABLE_MIN_CONST_1
INTEGRABLE_NEG
INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND
INTEGRABLE_ON_CONST
INTEGRABLE_ON_EMPTY
INTEGRABLE_ON_LITTLE_SUBINTERVALS
INTEGRABLE_ON_NULL
INTEGRABLE_ON_OPEN_INTERVAL
INTEGRABLE_ON_REFL
INTEGRABLE_ON_SUBDIVISION
INTEGRABLE_ON_SUBINTERVAL
INTEGRABLE_ON_SUPERSET
INTEGRABLE_PASTECART_SYM
INTEGRABLE_POINT_SPIKE
INTEGRABLE_REFLECT
INTEGRABLE_REFLECT_GEN
INTEGRABLE_RESTRICT
INTEGRABLE_RESTRICT_INTER
INTEGRABLE_RESTRICT_UNIV
INTEGRABLE_SPIKE
INTEGRABLE_SPIKE_EQ
INTEGRABLE_SPIKE_FINITE
INTEGRABLE_SPIKE_INTERIOR
INTEGRABLE_SPIKE_SET
INTEGRABLE_SPIKE_SET_EQ
INTEGRABLE_SPLIT
INTEGRABLE_SPLIT_SIDES
INTEGRABLE_STRADDLE
INTEGRABLE_STRADDLE_INTERVAL
INTEGRABLE_STRETCH
INTEGRABLE_SUB
INTEGRABLE_SUBINTERVAL
INTEGRABLE_SUBINTERVALS_IMP_MEASURABLE
INTEGRABLE_SUBINTERVALS_IMP_REAL_MEASURABLE
INTEGRABLE_SUBINTERVAL_LEFT
INTEGRABLE_SUBINTERVAL_RIGHT
INTEGRABLE_UNIFORM_LIMIT
INTEGRABLE_VSUM
INTEGRALS_EQ
INTEGRAL_0
INTEGRAL_ADD
INTEGRAL_BASIS_UNIMODULAR
INTEGRAL_BY_PARTS
INTEGRAL_CMUL
INTEGRAL_COMBINE
INTEGRAL_COMBINE_DIVISION_BOTTOMUP
INTEGRAL_COMBINE_DIVISION_TOPDOWN
INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP
INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN
INTEGRAL_COMPLEX_LMUL
INTEGRAL_COMPLEX_RMUL
INTEGRAL_COMPONENT
INTEGRAL_COMPONENT_LBOUND
INTEGRAL_COMPONENT_LE
INTEGRAL_COMPONENT_LE_AE
INTEGRAL_COMPONENT_POS
INTEGRAL_COMPONENT_UBOUND
INTEGRAL_CONST
INTEGRAL_DIFF
INTEGRAL_DROP_LE
INTEGRAL_DROP_LE_AE
INTEGRAL_DROP_LE_MEASURABLE
INTEGRAL_DROP_POS
INTEGRAL_DROP_POS_AE
INTEGRAL_EMPTY
INTEGRAL_EQ
INTEGRAL_EQ_0
INTEGRAL_EQ_HAS_INTEGRAL
INTEGRAL_HAS_VECTOR_DERIVATIVE
INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE
INTEGRAL_INTERVALS_DIFF_INCLUSION_EXCLUSION
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION_LEFT
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION_RIGHT
INTEGRAL_LE
INTEGRAL_LINEAR
INTEGRAL_LNORM_RPOW
INTEGRAL_MEASURE
INTEGRAL_MEASURE_UNIV
INTEGRAL_NEG
INTEGRAL_NORM_BOUND_INTEGRAL
INTEGRAL_NORM_BOUND_INTEGRAL_AE
INTEGRAL_NORM_BOUND_INTEGRAL_COMPONENT
INTEGRAL_NULL
INTEGRAL_OPEN_INTERVAL
INTEGRAL_PASTECART_CONST
INTEGRAL_PASTECART_CONTINUOUS
INTEGRAL_PASTECART_SYM
INTEGRAL_REFL
INTEGRAL_REFLECT
INTEGRAL_REFLECT_GEN
INTEGRAL_RESTRICT
INTEGRAL_RESTRICT_INTER
INTEGRAL_RESTRICT_UNIV
INTEGRAL_SPIKE
INTEGRAL_SPIKE_SET
INTEGRAL_SPLIT
INTEGRAL_SPLIT_SIGNED
INTEGRAL_SUB
INTEGRAL_SUBSET_COMPONENT_LE
INTEGRAL_SUBSET_DROP_LE
INTEGRAL_SWAP_CONTINUOUS
INTEGRAL_UNION
INTEGRAL_UNIQUE
INTEGRAL_VECTOR_ADD
INTEGRAL_VECTOR_ADD_LCANCEL
INTEGRAL_VECTOR_STDBASIS
INTEGRAL_VECTOR_SUB
INTEGRAL_VECTOR_VEC
INTEGRAL_VSUM
INTEGRATION_BY_PARTS
INTEGRATION_BY_PARTS_SIMPLE
INTER
INTERIOR_BALL
INTERIOR_BIJECTIVE_LINEAR_IMAGE
INTERIOR_CBALL
INTERIOR_CLOSED_EQ_EMPTY_AS_FRONTIER
INTERIOR_CLOSED_INTERVAL
INTERIOR_CLOSED_UNION_EMPTY_INTERIOR
INTERIOR_CLOSURE
INTERIOR_CLOSURE_IDEMP
INTERIOR_CLOSURE_INTER_OPEN
INTERIOR_COMPLEMENT
INTERIOR_CONVEX_HULL_3
INTERIOR_CONVEX_HULL_3_0
INTERIOR_CONVEX_HULL_3_MINIMAL
INTERIOR_CONVEX_HULL_EQ_EMPTY
INTERIOR_CONVEX_HULL_EXPLICIT
INTERIOR_CONVEX_HULL_EXPLICIT_MINIMAL
INTERIOR_DIFF
INTERIOR_EMPTY
INTERIOR_EQ
INTERIOR_EQ_EMPTY
INTERIOR_EQ_EMPTY_ALT
INTERIOR_FINITE_INTERS
INTERIOR_FRONTIER
INTERIOR_FRONTIER_EMPTY
INTERIOR_HALFSPACE_COMPONENT_GE
INTERIOR_HALFSPACE_COMPONENT_LE
INTERIOR_HALFSPACE_GE
INTERIOR_HALFSPACE_LE
INTERIOR_HYPERPLANE
INTERIOR_IMAGE_SUBSET
INTERIOR_INJECTIVE_LINEAR_IMAGE
INTERIOR_INSIDE_FRONTIER
INTERIOR_INTER
INTERIOR_INTERIOR
INTERIOR_INTERS_SUBSET
INTERIOR_INTERVAL
INTERIOR_LIMIT_POINT
INTERIOR_MAXIMAL
INTERIOR_MAXIMAL_EQ
INTERIOR_NEGATIONS
INTERIOR_OF_TRIANGLE
INTERIOR_OPEN
INTERIOR_PCROSS
INTERIOR_SEGMENT
INTERIOR_SIMPLEX_NONEMPTY
INTERIOR_SING
INTERIOR_STANDARD_HYPERPLANE
INTERIOR_STD_SIMPLEX
INTERIOR_SUBSET
INTERIOR_SUBSET_RELATIVE_INTERIOR
INTERIOR_SUBSET_UNION_INTERVALS
INTERIOR_SURJECTIVE_LINEAR_IMAGE
INTERIOR_TRANSLATION
INTERIOR_UNIONS_OPEN_SUBSETS
INTERIOR_UNION_EQ_EMPTY
INTERIOR_UNIQUE
INTERIOR_UNIV
INTERPMAT_LENGTH
INTERPMAT_POL_LENGTH
INTERPMAT_POL_LENGTH_LEM
INTERPMAT_SING
INTERPMAT_TRIO
INTERPMAT_TRIO_INNER
INTERPMAT_TRIO_TL
INTERPSIGNS_CONJ
INTERPSIGNS_SUBSET
INTERPSIGN_SUBSET
INTERP_CONST_NEG
INTERP_CONST_POS
INTERP_CONST_ZERO
INTERP_MIRROR
INTERP_MIRROR_LEMMA
INTERS
INTERS_0
INTERS_1
INTERS_2
INTERS_EMPTY
INTERS_EQ_EMPTY
INTERS_FACES_FINITE_ALTBOUND
INTERS_FACES_FINITE_BOUND
INTERS_GSPEC
INTERS_IMAGE
INTERS_INSERT
INTERS_OVER_UNIONS
INTERS_SUBSET
INTERS_SUBSET2
INTERS_SUMS_CLOSED_BALL_SEQUENTIAL
INTERS_UNION
INTERS_UNIONS
INTERVAL_0
INTERVAL_ABSV
INTERVAL_ABS_MAX
INTERVAL_ABS_MIN
INTERVAL_ADD
INTERVAL_BIJ_AFFINE
INTERVAL_BIJ_BIJ
INTERVAL_BISECTION
INTERVAL_BISECTION_STEP
INTERVAL_BOUNDS_EMPTY_1
INTERVAL_BOUNDS_NULL_1
INTERVAL_CASES_1
INTERVAL_CENTER
INTERVAL_CONTAINS_COMPACT_NEIGHBOURHOOD
INTERVAL_DIV
INTERVAL_DOUBLESPLIT
INTERVAL_EPS_0
INTERVAL_EPS_POS
INTERVAL_EQ_EMPTY
INTERVAL_EQ_EMPTY_1
INTERVAL_IMAGE_AFFINITY_INTERVAL
INTERVAL_IMAGE_STRETCH_INTERVAL
INTERVAL_INTER_HYPERPLANE
INTERVAL_LEMMA
INTERVAL_LEMMA_LT
INTERVAL_LOWERBOUND
INTERVAL_LOWERBOUND_1
INTERVAL_LOWERBOUND_NONEMPTY
INTERVAL_MAX
INTERVAL_MIN
INTERVAL_MINMAX
INTERVAL_MK
INTERVAL_MUL
INTERVAL_NEG
INTERVAL_NEG2
INTERVAL_NE_EMPTY
INTERVAL_NE_EMPTY_1
INTERVAL_NUM
INTERVAL_OF_TWOPOW
INTERVAL_OPEN_SUBSET_CLOSED
INTERVAL_REAL_INTERVAL
INTERVAL_SING
INTERVAL_SPLIT
INTERVAL_SSQRT
INTERVAL_SUB
INTERVAL_SUBDIVISION
INTERVAL_SUBSET_IS_INTERVAL
INTERVAL_TO_LESS
INTERVAL_TRANSLATION
INTERVAL_UPPERBOUND
INTERVAL_UPPERBOUND_1
INTERVAL_UPPERBOUND_NONEMPTY
INTERVAL_WIDTH
INTER_ACI
INTER_ASSOC
INTER_BALLS_EQ_EMPTY
INTER_COMM
INTER_EMPTY
INTER_FINITE
INTER_IDEMPOT
INTER_INTERIOR_UNIONS_INTERVALS
INTER_INTERVAL
INTER_INTERVAL_1
INTER_INTERVAL_MIXED_EQ_EMPTY
INTER_OVER_UNION
INTER_PCROSS
INTER_SEGMENT
INTER_SUBSET
INTER_THM
INTER_UNIONS
INTER_UNIV
INT_ABS
INT_ABS_0
INT_ABS_1
INT_ABS_ABS
INT_ABS_BETWEEN
INT_ABS_BETWEEN1
INT_ABS_BETWEEN2
INT_ABS_BOUND
INT_ABS_CASES
INT_ABS_CIRCLE
INT_ABS_LE
INT_ABS_MUL
INT_ABS_MUL_1
INT_ABS_NEG
INT_ABS_NEG_NUM
INT_ABS_NUM
INT_ABS_NZ
INT_ABS_POS
INT_ABS_POW
INT_ABS_REFL
INT_ABS_SGN
INT_ABS_SIGN
INT_ABS_SIGN2
INT_ABS_STILLNZ
INT_ABS_SUB
INT_ABS_SUB_ABS
INT_ABS_TRIANGLE
INT_ABS_ZERO
INT_ADD2_SUB2
INT_ADD_AC
INT_ADD_ASSOC
INT_ADD_LDISTRIB
INT_ADD_LID
INT_ADD_LINV
INT_ADD_NEG
INT_ADD_NEG_NUM
INT_ADD_NEGv2
INT_ADD_RDISTRIB
INT_ADD_RID
INT_ADD_RINV
INT_ADD_SUB
INT_ADD_SUB2
INT_ADD_SYM
INT_ARCH
INT_BEZOUT_PRIME
INT_BOUNDS_LE
INT_BOUNDS_LT
INT_CHINESE_REMAINDER
INT_CHINESE_REMAINDER_COPRIME
INT_CHINESE_REMAINDER_COPRIME_UNIQUE
INT_CHINESE_REMAINDER_USUAL
INT_CONG
INT_CONG_0
INT_CONG_0_DIVIDES
INT_CONG_1_DIVIDES
INT_CONG_ADD
INT_CONG_ADD_LCANCEL
INT_CONG_ADD_LCANCEL_EQ
INT_CONG_ADD_LCANCEL_EQ_0
INT_CONG_ADD_RCANCEL
INT_CONG_ADD_RCANCEL_EQ
INT_CONG_ADD_RCANCEL_EQ_0
INT_CONG_CHINESE
INT_CONG_COPRIME
INT_CONG_DIVIDES
INT_CONG_IMP_EQ
INT_CONG_INT_DIVIDES_MODULUS
INT_CONG_MOD_0
INT_CONG_MOD_1
INT_CONG_MOD_MULT
INT_CONG_MUL
INT_CONG_MUL_LCANCEL
INT_CONG_MUL_LCANCEL_EQ
INT_CONG_MUL_RCANCEL
INT_CONG_MUL_RCANCEL_EQ
INT_CONG_POW
INT_CONG_REFL
INT_CONG_SOLVE
INT_CONG_SOLVE_POS
INT_CONG_SOLVE_UNIQUE
INT_CONG_SUB
INT_CONG_SYM
INT_CONG_TO_1
INT_CONG_TRANS
INT_COPRIME_0
INT_COPRIME_1
INT_COPRIME_ABS
INT_COPRIME_BEZOUT
INT_COPRIME_BEZOUT_ALT
INT_COPRIME_DIVISORS
INT_COPRIME_DIVPROD
INT_COPRIME_GCD
INT_COPRIME_LABS
INT_COPRIME_LMUL
INT_COPRIME_LMUL2
INT_COPRIME_LNEG
INT_COPRIME_LPOW
INT_COPRIME_MINUS1
INT_COPRIME_MUL
INT_COPRIME_NEG
INT_COPRIME_PLUS1
INT_COPRIME_POW
INT_COPRIME_POW2
INT_COPRIME_POW_ABS
INT_COPRIME_POW_DIVPROD
INT_COPRIME_POW_IMP
INT_COPRIME_POW_ODD
INT_COPRIME_PRIME
INT_COPRIME_PRIMEPOW
INT_COPRIME_PRIME_EQ
INT_COPRIME_RABS
INT_COPRIME_REFL
INT_COPRIME_RMUL
INT_COPRIME_RMUL2
INT_COPRIME_RNEG
INT_COPRIME_RPOW
INT_COPRIME_SOS
INT_COPRIME_SYM
INT_CRT_STRONG
INT_CRT_STRONG_IFF
INT_DIFFSQ
INT_DISTINCT_PRIME_COPRIME
INT_DIVIDES_ABS
INT_DIVIDES_ANTISYM
INT_DIVIDES_ANTISYM_ABS
INT_DIVIDES_ANTISYM_ASSOCIATED
INT_DIVIDES_ANTISYM_DIVISORS
INT_DIVIDES_ANTISYM_POS
INT_DIVIDES_FACT
INT_DIVIDES_FACT_PRIME
INT_DIVIDES_GCD
INT_DIVIDES_GCD_LEFT
INT_DIVIDES_GCD_RIGHT
INT_DIVIDES_IMP_ABS_NUM_DIVIDES
INT_DIVIDES_LABS
INT_DIVIDES_LE
INT_DIVIDES_MUL
INT_DIVIDES_NUM
INT_DIVIDES_ONE
INT_DIVIDES_ONE_ABS
INT_DIVIDES_ONE_POS
INT_DIVIDES_POW
INT_DIVIDES_POW2
INT_DIVIDES_POW2_EQ
INT_DIVIDES_POW2_REV
INT_DIVIDES_POW_LE
INT_DIVIDES_PRIME_POW_LE
INT_DIVIDES_PRIME_PRIME
INT_DIVIDES_PSUM
INT_DIVIDES_RABS
INT_DIVIDES_RPOW
INT_DIVIDES_RPOW_SUC
INT_DIVISION
INT_DIVISION_0
INT_DIVISION_DECOMP
INT_DIVISORS_RECURRENCE
INT_DIVMOD_EXIST_0
INT_DIVMOD_UNIQ
INT_DOWN2
INT_DOWN_MUL_LT
INT_ENTIRE
INT_EQ_ADD_LCANCEL
INT_EQ_ADD_LCANCEL_0
INT_EQ_ADD_RCANCEL
INT_EQ_ADD_RCANCEL_0
INT_EQ_IMP_CONG
INT_EQ_IMP_LE
INT_EQ_MUL_LCANCEL
INT_EQ_MUL_RCANCEL
INT_EQ_NEG2
INT_EQ_PRIME_POW_ABS
INT_EQ_PRIME_POW_POS
INT_EQ_SGN_ABS
INT_EQ_SQUARE_ABS
INT_EQ_SUB_LADD
INT_EQ_SUB_RADD
INT_EUCLID
INT_EUCLID_BOUND
INT_EXISTS_ABS
INT_EXISTS_CASES
INT_EXISTS_POS
INT_FORALL_ABS
INT_FORALL_POS
INT_GCD_0
INT_GCD_1
INT_GCD_ABS
INT_GCD_ADD
INT_GCD_ASSOC
INT_GCD_BEZOUT
INT_GCD_COPRIME
INT_GCD_COPRIME_EXISTS
INT_GCD_DIVIDES
INT_GCD_EQ_0
INT_GCD_EXISTS
INT_GCD_EXISTS_POS
INT_GCD_POS
INT_GCD_RECURRENCE
INT_GCD_REFL
INT_GCD_SUB
INT_GCD_SYM
INT_GCD_UNIQUE
INT_GCD_UNIQUE_ABS
INT_GE
INT_GT
INT_GT_DISCRETE
INT_IMAGE
INT_INT
INT_INTEGRAL
INT_IS_INT
INT_LET_ADD
INT_LET_ADD2
INT_LET_ANTISYM
INT_LET_TOTAL
INT_LET_TRANS
INT_LE_01
INT_LE_ADD
INT_LE_ADD2
INT_LE_ADDL
INT_LE_ADDR
INT_LE_ANTISYM
INT_LE_DOUBLE
INT_LE_LADD
INT_LE_LADD_IMP
INT_LE_LMUL
INT_LE_LNEG
INT_LE_LT
INT_LE_MAX
INT_LE_MIN
INT_LE_MUL
INT_LE_MUL_EQ
INT_LE_NEG
INT_LE_NEG2
INT_LE_NEGL
INT_LE_NEGR
INT_LE_NEGTOTAL
INT_LE_POW2
INT_LE_RADD
INT_LE_REFL
INT_LE_RMUL
INT_LE_RNEG
INT_LE_SQUARE
INT_LE_SQUARE_ABS
INT_LE_SUB_LADD
INT_LE_SUB_RADD
INT_LE_TOTAL
INT_LE_TRANS
INT_LINEAR_CONG_POS
INT_LNEG_UNIQ
INT_LT
INT_LTE_ADD
INT_LTE_ADD2
INT_LTE_ANTISYM
INT_LTE_TOTAL
INT_LTE_TRANS
INT_LT_01
INT_LT_ADD
INT_LT_ADD1
INT_LT_ADD2
INT_LT_ADDL
INT_LT_ADDNEG
INT_LT_ADDNEG2
INT_LT_ADDR
INT_LT_ADD_SUB
INT_LT_ANTISYM
INT_LT_DISCRETE
INT_LT_GT
INT_LT_IMP_LE
INT_LT_IMP_NE
INT_LT_LADD
INT_LT_LE
INT_LT_LMUL_EQ
INT_LT_MAX
INT_LT_MIN
INT_LT_MUL
INT_LT_MUL_EQ
INT_LT_NEG
INT_LT_NEG2
INT_LT_NEGTOTAL
INT_LT_POW2
INT_LT_RADD
INT_LT_REFL
INT_LT_RMUL_EQ
INT_LT_SQUARE_ABS
INT_LT_SUB_LADD
INT_LT_SUB_RADD
INT_LT_TOTAL
INT_LT_TRANS
INT_MAX_ACI
INT_MAX_ASSOC
INT_MAX_LE
INT_MAX_LT
INT_MAX_MAX
INT_MAX_MIN
INT_MAX_SYM
INT_MIN_ACI
INT_MIN_ASSOC
INT_MIN_LE
INT_MIN_LT
INT_MIN_MAX
INT_MIN_MIN
INT_MIN_SYM
INT_MOD_LEMMA
INT_MUL_AC
INT_MUL_ASSOC
INT_MUL_LID
INT_MUL_LNEG
INT_MUL_LZERO
INT_MUL_POS_LE
INT_MUL_POS_LT
INT_MUL_RID
INT_MUL_RNEG
INT_MUL_RZERO
INT_MUL_SYM
INT_NEGNEG
INT_NEG_0
INT_NEG_ADD
INT_NEG_EQ
INT_NEG_EQ_0
INT_NEG_GE0
INT_NEG_GT0
INT_NEG_LE0
INT_NEG_LMUL
INT_NEG_LT0
INT_NEG_MINUS1
INT_NEG_MUL2
INT_NEG_NEG
INT_NEG_RMUL
INT_NEG_SUB
INT_NN_NEG
INT_NOT_EQ
INT_NOT_LE
INT_NOT_LT
INT_NUM
INT_NUM_REAL
INT_OF_NUM_ADD
INT_OF_NUM_DEST
INT_OF_NUM_EQ
INT_OF_NUM_EXISTS
INT_OF_NUM_GE
INT_OF_NUM_GT
INT_OF_NUM_LE
INT_OF_NUM_LT
INT_OF_NUM_MAX
INT_OF_NUM_MIN
INT_OF_NUM_MUL
INT_OF_NUM_OF_INT
INT_OF_NUM_POW
INT_OF_NUM_SUB
INT_OF_NUM_SUC
INT_OF_REAL_ADD
INT_OF_REAL_MUL
INT_OF_REAL_NEG_INT_OF_NUM
INT_OF_REAL_NEG_NUM
INT_OF_REAL_OF_INT
INT_POLY_DIFF_EXPLICIT
INT_POLY_LAGRANGE
INT_POS
INT_POS'
INT_POS_NEG
INT_POS_NZ
INT_POW
INT_POW2_ABS
INT_POW_1
INT_POW_1_LE
INT_POW_1_LT
INT_POW_2
INT_POW_ADD
INT_POW_EQ
INT_POW_EQ_0
INT_POW_EQ_ABS
INT_POW_EVEN_NEG1
INT_POW_LE
INT_POW_LE2
INT_POW_LE2_ODD
INT_POW_LE2_REV
INT_POW_LE_1
INT_POW_LT
INT_POW_LT2
INT_POW_LT2_REV
INT_POW_LT_1
INT_POW_MONO
INT_POW_MONO_LT
INT_POW_MUL
INT_POW_MUL_EXISTS
INT_POW_NEG
INT_POW_NEG1
INT_POW_NZ
INT_POW_ODD_NEG1
INT_POW_ONE
INT_POW_POW
INT_POW_ZERO
INT_PRIME
INT_PRIMES_INFINITE
INT_PRIME_0
INT_PRIME_1
INT_PRIME_2
INT_PRIME_ABS
INT_PRIME_COPRIME
INT_PRIME_COPRIME_CASES
INT_PRIME_COPRIME_EQ
INT_PRIME_COPRIME_LT
INT_PRIME_DIVPOW
INT_PRIME_DIVPOW_N
INT_PRIME_DIVPROD
INT_PRIME_DIVPROD_EQ
INT_PRIME_DIVPROD_POW
INT_PRIME_FACTOR
INT_PRIME_FACTOR_INDUCT
INT_PRIME_FACTOR_LT
INT_PRIME_GE_2
INT_PRIME_IMP_NZ
INT_PRIME_NEG
INT_PRIME_NUM_PRIME
INT_REP
INT_REP2
INT_REP3
INT_RNEG_UNIQ
INT_SGN
INT_SGN_0
INT_SGN_ABS
INT_SGN_CASES
INT_SGN_EQ
INT_SGN_INEQS
INT_SGN_INT_SGN
INT_SGN_MUL
INT_SGN_NEG
INT_SGN_POW
INT_SGN_POW_2
INT_SOS_EQ_0
INT_SUB
INT_SUB_0
INT_SUB_ABS
INT_SUB_ADD
INT_SUB_ADD2
INT_SUB_LDISTRIB
INT_SUB_LE
INT_SUB_LNEG
INT_SUB_LT
INT_SUB_LZERO
INT_SUB_NEG2
INT_SUB_POW
INT_SUB_POW_L1
INT_SUB_POW_R1
INT_SUB_RDISTRIB
INT_SUB_REFL
INT_SUB_RNEG
INT_SUB_RZERO
INT_SUB_SUB
INT_SUB_SUB2
INT_SUB_TRIANGLE
INT_WOP
INT_ZERO
INT_ZERO_NEG
INV
INVARIANCE_OF_DIMENSION
INVARIANCE_OF_DIMENSION_AFFINE_SETS
INVARIANCE_OF_DIMENSION_CONVEX_DOMAIN
INVARIANCE_OF_DIMENSION_SUBSPACES
INVARIANCE_OF_DOMAIN
INVARIANCE_OF_DOMAIN_AFFINE_SETS
INVARIANCE_OF_DOMAIN_GEN
INVARIANCE_OF_DOMAIN_HOMEOMORPHIC
INVARIANCE_OF_DOMAIN_HOMEOMORPHISM
INVARIANCE_OF_DOMAIN_SPHERE_AFFINE_SET
INVARIANCE_OF_DOMAIN_SPHERE_AFFINE_SET_GEN
INVARIANCE_OF_DOMAIN_SUBSPACES
INVERSE_BIJ
INVERSE_DEF
INVERSE_FN
INVERSE_FUNCTION_C1
INVERSE_I
INVERSE_SWAP
INVERSE_UNIQUE_o
INVERSE_XY
INVERTIBLE_COFACTOR
INVERTIBLE_DET_NZ
INVERTIBLE_FIXPOINT_PROPERTY
INVERTIBLE_IMP_SQUARE_MATRIX
INVERTIBLE_LEFT_INVERSE
INVERTIBLE_MATRIX_MUL
INVERTIBLE_NEG
INVERTIBLE_RIGHT_INVERSE
INVERTIBLE_TRANSP
INVOLUTION_DELETE
INVOLUTION_EVEN
INVOLUTION_EVEN_INDUCT
INVOLUTION_EVEN_STEP
INVOLUTION_FIX_FIX
INVOLUTION_FIX_ODD
INVOLUTION_IMAGE
INVOLUTION_NOFIXES
INVOLUTION_ODD
INVOLUTION_STEPDOWN
INVOLUTION_SUBSET
INV_POLY_CMUL
INV_POLY_CMUL2
INV_homeomorphism
IN_AFFINE_ADD_MUL
IN_AFFINE_ADD_MUL_DIFF
IN_AFFINE_HULL_LINEAR_IMAGE
IN_AFFINE_MUL_DIFF_ADD
IN_AFFINE_SUB_MUL_DIFF
IN_AFFSIGN
IN_AFFSIGN_TRANSLATION
IN_BALL
IN_BALL_0
IN_BALL_IM
IN_BALL_RE
IN_BOOL
IN_CARD_ADD
IN_CARD_MUL
IN_CBALL
IN_CBALL_0
IN_CBALL_IM
IN_CBALL_RE
IN_CLOSURE_CONNECTED_COMPONENT
IN_CLOSURE_DELETE
IN_COMPONENTS
IN_COMPONENTS_CONNECTED
IN_COMPONENTS_MAXIMAL
IN_COMPONENTS_NONEMPTY
IN_COMPONENTS_SELF
IN_COMPONENTS_SUBSET
IN_COMPONENTS_UNIONS_COMPLEMENT
IN_COMPREHENSION
IN_CONVEX_HULL_EXCHANGE
IN_CONVEX_HULL_EXCHANGE_UNIQUE
IN_CONVEX_HULL_LINEAR_IMAGE
IN_CONVEX_SET
IN_CROSS
IN_DELETE
IN_DELETE_EQ
IN_DIFF
IN_DIMINDEX_SWAP
IN_DIRECTION
IN_DISJOINT
IN_ELIM_PAIR_THM
IN_ELIM_PASTECART_THM
IN_ELIM_THM
IN_EPIGRAPH
IN_FROM
IN_FRONTIER_CONVEX_HULL
IN_IMAGE
IN_IMAGE_DROPOUT
IN_IMAGE_LIFT_DROP
IN_INSERT
IN_INTER
IN_INTERIOR
IN_INTERIOR_CBALL
IN_INTERIOR_CLOSURE_CONVEX_SEGMENT
IN_INTERIOR_CLOSURE_CONVEX_SHRINK
IN_INTERIOR_CONVEX_SHRINK
IN_INTERIOR_LINEAR_IMAGE
IN_INTERS
IN_INTERVAL
IN_INTERVAL_1
IN_INTERVAL_INTERVAL_BIJ
IN_INTERVAL_REFLECT
IN_NUMSEG
IN_NUMSEG_0
IN_NUMSEG_1
IN_NUMSEG_RESTRICT_FALSE
IN_OPEN_SEGMENT
IN_OPEN_SEGMENT_ALT
IN_PATH_IMAGE_PARTCIRCLEPATH
IN_POWERSET
IN_PRODUCT
IN_RADICALS_SMALLER
IN_REAL_INTERVAL
IN_REAL_INTERVAL_REFLECT
IN_REAL_SEGMENT
IN_RELATIVE_INTERIOR
IN_RELATIVE_INTERIOR_CBALL
IN_RELATIVE_INTERIOR_CLOSURE_CONVEX_SEGMENT
IN_RELATIVE_INTERIOR_CLOSURE_CONVEX_SHRINK
IN_RELATIVE_INTERIOR_CONVEX_SHRINK
IN_REST
IN_SEGMENT
IN_SEGMENT_COMPONENT
IN_SEGMENT_CX
IN_SEGMENT_CX_GEN
IN_SET_ELEMENT
IN_SET_OF_LIST
IN_SING
IN_SLICE
IN_SPAN_DELETE
IN_SPAN_IMAGE_BASIS
IN_SPAN_INSERT
IN_SPHERE
IN_SPHERE_0
IN_SUPPORT
IN_TRIPLE
IN_UNION
IN_UNIONS
IN_UNIV
IRRATIONAL_APPROXIMATION
IRRATIONAL_SQRT_2
IRRATIONAL_SQRT_NONSQUARE
IRRATIONAL_SQRT_PRIME
ISAFFORM
ISAFTERM
ISMET_R1
ISO
ISOLATED_ZEROS
ISOMETRIES_SUBSPACES
ISOMETRY_IMP_AFFINITY
ISOMETRY_IMP_EMBEDDING
ISOMETRY_IMP_HOMEOMORPHISM_COMPACT
ISOMETRY_IMP_OPEN_MAP
ISOMETRY_LINEAR
ISOMETRY_ON_IMP_CONTINUOUS_ON
ISOMETRY_SPHERE_EXTEND
ISOMETRY_SUBSET_SUBSPACE
ISOMETRY_SUBSPACES
ISOMETRY_UNIV_SUBSPACE
ISOMETRY_UNIV_SUPERSET_SUBSPACE
ISOMETRY_UNIV_UNIV
ISOMORPHISMS_UNIV_UNIV
ISOMORPHISM_EXPAND
ISOSCELES_TRIANGLE_1
ISOSCELES_TRIANGLE_2
ISOSCELES_TRIANGLE_3
ISOSCELES_TRIANGLE_4
ISOSCELES_TRIANGLE_5
ISOSCELES_TRIANGLE_6
ISOSCELES_TRIANGLE_CONVERSE
ISOSCELES_TRIANGLE_THEOREM
ISO_FUN
ISO_REFL
ISO_USAGE
ISQRT
ISQRT_0
ISQRT_SUC
ISQRT_UNIQUE
ISQRT_WORKS
ISTOPLOGY_SUBTOPOLOGY
ISTOPOLOGY_OPEN_IN
ISUM_0
ISUM_ABS
ISUM_ABS_BOUND
ISUM_ABS_LE
ISUM_ABS_NUMSEG
ISUM_ADD
ISUM_ADD_NUMSEG
ISUM_ADD_SPLIT
ISUM_BIJECTION
ISUM_BOUND
ISUM_BOUND_LT
ISUM_BOUND_LT_ALL
ISUM_CASES
ISUM_CLAUSES
ISUM_CLAUSES_LEFT
ISUM_CLAUSES_NUMSEG
ISUM_CLAUSES_RIGHT
ISUM_COMBINE_L
ISUM_COMBINE_R
ISUM_CONST
ISUM_CONST_NUMSEG
ISUM_DELETE
ISUM_DELETE_CASES
ISUM_DELTA
ISUM_DIFF
ISUM_DIFFS
ISUM_EQ
ISUM_EQ_0
ISUM_EQ_0_NUMSEG
ISUM_EQ_GENERAL
ISUM_EQ_GENERAL_INVERSES
ISUM_EQ_NUMSEG
ISUM_EQ_SUPERSET
ISUM_GROUP
ISUM_IMAGE
ISUM_IMAGE_GEN
ISUM_IMAGE_LE
ISUM_IMAGE_NONZERO
ISUM_INCL_EXCL
ISUM_INJECTION
ISUM_ISUM_PRODUCT
ISUM_ISUM_RESTRICT
ISUM_LE
ISUM_LE_INCLUDED
ISUM_LE_NUMSEG
ISUM_LMUL
ISUM_LT
ISUM_LT_ALL
ISUM_MULTICOUNT
ISUM_MULTICOUNT_GEN
ISUM_NEG
ISUM_OFFSET
ISUM_OFFSET_0
ISUM_PARTIAL_PRE
ISUM_PARTIAL_SUC
ISUM_POS_BOUND
ISUM_POS_EQ_0
ISUM_POS_EQ_0_NUMSEG
ISUM_POS_LE
ISUM_POS_LE_NUMSEG
ISUM_RESTRICT
ISUM_RESTRICT_SET
ISUM_RMUL
ISUM_SING
ISUM_SING_NUMSEG
ISUM_SUB
ISUM_SUBSET
ISUM_SUBSET_SIMPLE
ISUM_SUB_NUMSEG
ISUM_SUPERSET
ISUM_SUPPORT
ISUM_SWAP
ISUM_SWAP_NUMSEG
ISUM_TRIV_NUMSEG
ISUM_UNION
ISUM_UNIONS_NONZERO
ISUM_UNION_EQ
ISUM_UNION_LZERO
ISUM_UNION_NONZERO
ISUM_UNION_RZERO
ISUM_ZERO_EXISTS
IS_AFFINE_HULL
IS_CLASH
IS_CONVEX_HULL
IS_HULL
IS_INTERVAL_1
IS_INTERVAL_1_CASES
IS_INTERVAL_COMPACT
IS_INTERVAL_CONNECTED
IS_INTERVAL_CONNECTED_1
IS_INTERVAL_CONTRACTIBLE_1
IS_INTERVAL_CONVEX
IS_INTERVAL_CONVEX_1
IS_INTERVAL_EMPTY
IS_INTERVAL_IMP_LOCALLY_COMPACT
IS_INTERVAL_INTER
IS_INTERVAL_INTERVAL
IS_INTERVAL_PATH_CONNECTED
IS_INTERVAL_PATH_CONNECTED_1
IS_INTERVAL_PCROSS
IS_INTERVAL_PCROSS_EQ
IS_INTERVAL_POINTWISE
IS_INTERVAL_SCALING
IS_INTERVAL_SCALING_EQ
IS_INTERVAL_SIMPLY_CONNECTED_1
IS_INTERVAL_SING
IS_INTERVAL_SUMS
IS_INTERVAL_TRANSLATION
IS_INTERVAL_TRANSLATION_EQ
IS_INTERVAL_UNIV
IS_INT_FACT_DIV
IS_INT_FACT_DIV_FACT_DIV_FACT
IS_INT_NZ_ABS_GE_1
IS_INT_POLY
IS_INT_POLY_NUKE
IS_INT_SUM
IS_QUADRATIC_RESIDUE
IS_QUADRATIC_RESIDUE_COMMON
IS_QUADRATIC_RESIDUE_PAIR
IS_REALINTERVAL_CONNECTED
IS_REALINTERVAL_CONTAINS_SEGMENT_EQ
IS_REALINTERVAL_CONTAINS_SEGMENT_IMP
IS_REALINTERVAL_CONTINUOUS_IMAGE
IS_REALINTERVAL_CONVEX
IS_REALINTERVAL_CONVEX_COMPLEX
IS_REALINTERVAL_EMPTY
IS_REALINTERVAL_INTERVAL
IS_REALINTERVAL_IS_INTERVAL
IS_REALINTERVAL_SEGMENT
IS_REALINTERVAL_UNION
IS_REALINTERVAL_UNIV
IS_REAL_INTERVAL_CASES
IS_REAL_INTERVAL_CONTAINS_SEGMENT
IS_RESULT
ITCHY_LEMMA
ITER
ITERATE_AND
ITERATE_BIJECTION
ITERATE_CASES
ITERATE_CLAUSES
ITERATE_CLAUSES_GEN
ITERATE_CLAUSES_NUMSEG
ITERATE_CLOSED
ITERATE_DELETE
ITERATE_DELTA
ITERATE_DIFF
ITERATE_DIFF_GEN
ITERATE_EQ
ITERATE_EQ_GENERAL
ITERATE_EQ_GENERAL_INVERSES
ITERATE_EQ_NEUTRAL
ITERATE_EXPAND_CASES
ITERATE_IMAGE
ITERATE_IMAGE_NONZERO
ITERATE_INCL_EXCL
ITERATE_INJECTION
ITERATE_ITERATE_PRODUCT
ITERATE_NONZERO_IMAGE_LEMMA
ITERATE_OP
ITERATE_OP_GEN
ITERATE_PAIR
ITERATE_PERMUTE
ITERATE_POLY_ADD_PRE_REC
ITERATE_RADD_POLYADD
ITERATE_RELATED
ITERATE_SING
ITERATE_SOME
ITERATE_SUC_REC
ITERATE_SUPERSET
ITERATE_SUPPORT
ITERATE_UNION
ITERATE_UNION_GEN
ITERATE_UNION_NONZERO
ITER_1
ITER_ADD
ITER_ALT
ITER_ALT_POINTLESS
ITER_DIFFS_LEMMA
ITER_FIXPOINT
ITER_INT
ITER_INT0
ITER_MUL
ITER_PAR
ITER_PAR0
ITER_POINTLESS
ITER_ROTATE_ABOUT
ITER_SEQ
ITER_SEQ0
ITE_INDUCT
ITLIST
ITLIST2
ITLIST2_0_LEMMA
ITLIST2_DEF
ITLIST_APPEND
ITLIST_EXTRA
ITLIST_VALMOD_EQ
ITLIST_VALMOD_FILTER
ITSET
ITSET_EQ
ITSET_MODMULT
ITSET_MODMULT_COPRIME
IVT
IVT2
IVT_DECREASING_COMPONENT_1
IVT_DECREASING_COMPONENT_ON_1
IVT_DECREASING_IM
IVT_DECREASING_RE
IVT_DERIVATIVE_0
IVT_DERIVATIVE_NEG
IVT_DERIVATIVE_POS
IVT_INCREASING_COMPONENT_1
IVT_INCREASING_COMPONENT_ON_1
IVT_INCREASING_IM
IVT_INCREASING_RE
IVT_LEMMA1
IVT_LEMMA2
I_AXIOM
I_BIJ
I_BOOL_EXISTS
I_DEF
I_IND_EXISTS
I_INFINITE
I_O_ID
I_PAIR_EXISTS
I_SET
I_SET_EXISTS
I_SET_SETLEVEL
I_THM
InteriorAngle_DEF
InteriorCircle_DEF
InteriorTriangle_DEF
Interval_DEF
ichoose
icongruence
icongruence_general
icongruence_var
id
iexists
if_def
iff_def
iff_imp1
iff_imp2
iff_refl
iff_sym
iff_thm_nn
iff_thm_np
iff_thm_pn
iff_thm_pp
iff_trans
ii
image_app
image_compact
image_curve_cell_reflA
image_curve_cell_reflB
image_curve_cell_reflC
image_delete_choice
image_domain_sub
image_empty
image_imp
image_inj
image_interval
image_interval2
image_inv_image
image_power_inj
image_power_surj
image_powerset
image_preimage
image_sing
image_top
image_unions
imp_add_assum
imp_add_concl
imp_antisym
imp_contr
imp_contrf
imp_def
imp_false_rule
imp_insert
imp_mono_th
imp_refl
imp_swap
imp_swap_th
imp_thm_n
imp_thm_pn
imp_thm_pp
imp_trans
imp_trans2
imp_trans_chain_2
imp_trans_th
imp_true_rule
imp_truefalse
imp_unduplicate
impex
in_direction
in_pair
in_preimage
in_union
inacc_tybij_th
incf_V
incf_value
ind_model_tybij_th
independent
index
index_def
indicator
indinv
indset
induced_compact
induced_top_interval
induced_top_open
induced_top_support
induced_top_top
induced_top_unions
induced_trans
inductive_diff
inductive_inter
inductive_segment
inductive_set_adj
inductive_set_endpoint
inductive_set_join
inductive_set_restrict
inductive_univ
inf
inf_LB
inf_eps
inf_unique
inferisign_lem00
infinite_closed_interval
infinite_image
infinite_int
infinite_interval
infinite_intpair
infinite_subset
infnorm
infsum
init
inj_bij
inj_bij_size
inj_domain_sub
inj_image_subset
inj_inter
inj_split
inj_subset
inj_subset2
inj_subset_domain
inj_terminal
inner
inseg
insert_sing
inset
inside
inst_INDUCT,inst_RECURSION
instantiation
int2_range_finite
int7
int9
int_abs
int_abs_th
int_add
int_add_th
int_arch
int_congruent
int_coprime
int_divides
int_eq
int_gcd
int_ge
int_gt
int_isum
int_le
int_le_mp
int_lt
int_lt_suc_le
int_max
int_max_th
int_min
int_min_th
int_mod
int_mul
int_mul_th
int_neg
int_neg_num_th
int_neg_th
int_of_num
int_of_num_th
int_pow
int_pow2_gt1
int_pow_th
int_prime
int_range_finite
int_sgn
int_sgn_th
int_sub
int_sub_th
int_suc
integer
integer_cube_finite
integrable
integrable_on
integral
integral_vector
inter_lattice
inter_midpoint
inter_union
interior
interp
interp_doub
interp_sing
interpmat
interpsign
interpsigns
inters_inter
inters_singleton
inters_subset
interval
interval_bij
interval_closed
interval_closed_ball
interval_compact
interval_eq
interval_euclid1_bounded
interval_euclid1_closed
interval_euclid1_compact
interval_finite
interval_image
interval_lowerbound
interval_subset
interval_upperbound
inv_comp_left
inv_comp_right
inv_twopow
inverse
invertible
invo_BIJ
invo_homeo
involution
ips_gt_nz_thm
ips_lt_nz_thm
is_int
is_intersection
is_interval
is_midpoint
is_nadd
is_nadd_0
is_quadratic_residue
is_realinterval
is_sphere
isafform
isafterm
isagform
isagterm
isaprove
isaset
isasetlevel
ismet
iso_eps_support0
iso_int_model_lemma
iso_support_eps_finite
iso_support_eps_min
iso_support_eps_nonempty
iso_support_min_int
isoth,rclauses
isotropic
ispec
ispec_lemma
isthree
istopology
isubst
isubst_general
isubst_var
isum
ite_INDUCT,ite_RECURSION
ite_def
iter_rhs
iterate
ith,rth