HOL html

Files Index

Theorems Index

I (theorems)

IDEMPOTENT_IMP_RETRACTION
II_NZ
IM
IMAGE_AFFINITY_INTERVAL
IMAGE_AFFINITY_REAL_INTERVAL
IMAGE_CLOSURE_SUBSET
IMAGE_CX
IMAGE_DROPOUT_CLOSED_INTERVAL
IMAGE_DROP_INTERVAL
IMAGE_DROP_UNIV
IMAGE_LEMMA_0
IMAGE_LEMMA_1
IMAGE_LEMMA_2
IMAGE_LIFT_DROP
IMAGE_LIFT_REAL_INTERVAL
IMAGE_LIFT_REAL_SEGMENT
IMAGE_LIFT_UNIV
IMAGE_STRETCH_INTERVAL
IMAGE_STRETCH_REAL_INTERVAL
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
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
INDUCT_LINEAR_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY
INDUCT_MATRIX_ELEMENTARY_ALT
INDUCT_MATRIX_ROW_OPERATIONS
INESSENTIAL_EQ_CONTINUOUS_LOGARITHM
INESSENTIAL_EQ_CONTINUOUS_LOGARITHM_CIRCLE
INESSENTIAL_EQ_EXTENSIBLE
INESSENTIAL_IMP_CONTINUOUS_LOGARITHM_CIRCLE
INESSENTIAL_IMP_UNICOHERENT
INESSENTIAL_SPHEREMAP_2
INESSENTIAL_SPHEREMAP_LOWDIM
INESSENTIAL_SPHEREMAP_LOWDIM_GEN
INFINITE_ARC_IMAGE
INFINITE_ENUMERATE
INFINITE_FROM
INFINITE_OPEN_IN
INFINITE_SIMPLE_PATH_IMAGE
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_INSERT
INJECTIVE_EQ_1D_OPEN_MAP_UNIV
INJECTIVE_IMP_ISOMETRIC
INJECTIVE_INTO_1D_EQ_HOMEOMORPHISM
INJECTIVE_INTO_1D_IMP_OPEN_MAP
INJECTIVE_INTO_1D_IMP_OPEN_MAP_UNIV
INJECTIVE_MAP_OPEN_IFF_CLOSED
INJECTIVE_PAD2D3D
INJECTIVE_SCALING
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_LINEAR_IMAGE
INSIDE_MONO
INSIDE_NO_OVERLAP
INSIDE_OF_TRIANGLE
INSIDE_OUTSIDE
INSIDE_OUTSIDE_INTERSECT_CONNECTED
INSIDE_OUTSIDE_UNIQUE
INSIDE_SAME_COMPONENT
INSIDE_SIMPLE_CURVE_IMP_CLOSED
INSIDE_SUBSET
INSIDE_TRANSLATION
INSIDE_UNION_OUTSIDE
INSIDE_UNIQUE
INTEGER_DET
INTEGER_PRODUCT
INTEGER_SIGN
INTEGER_WINDING_NUMBER
INTEGER_WINDING_NUMBER_EQ
INTEGRABLE_0
INTEGRABLE_ADD
INTEGRABLE_AFFINITY
INTEGRABLE_ALT
INTEGRABLE_ALT_SUBSET
INTEGRABLE_CAUCHY
INTEGRABLE_CCONTINUOUS_EXPLICIT
INTEGRABLE_CCONTINUOUS_EXPLICIT_SYMMETRIC
INTEGRABLE_CMUL
INTEGRABLE_COMBINE
INTEGRABLE_COMBINE_DIVISION
INTEGRABLE_COMPONENTWISE
INTEGRABLE_CONST
INTEGRABLE_CONTINUOUS
INTEGRABLE_DECREASING
INTEGRABLE_DECREASING_1
INTEGRABLE_DECREASING_PRODUCT
INTEGRABLE_DECREASING_PRODUCT_UNIV
INTEGRABLE_EQ
INTEGRABLE_IMP_MEASURABLE
INTEGRABLE_IMP_REAL_MEASURABLE
INTEGRABLE_INCREASING
INTEGRABLE_INCREASING_1
INTEGRABLE_INCREASING_PRODUCT
INTEGRABLE_INCREASING_PRODUCT_UNIV
INTEGRABLE_INTEGRAL
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_REFLECT
INTEGRABLE_RESTRICT
INTEGRABLE_RESTRICT_INTER
INTEGRABLE_RESTRICT_UNIV
INTEGRABLE_SPIKE
INTEGRABLE_SPIKE_FINITE
INTEGRABLE_SPIKE_INTERIOR
INTEGRABLE_SPIKE_SET
INTEGRABLE_SPIKE_SET_EQ
INTEGRABLE_SPLIT
INTEGRABLE_STRADDLE
INTEGRABLE_STRADDLE_INTERVAL
INTEGRABLE_STRETCH
INTEGRABLE_SUB
INTEGRABLE_SUBINTERVAL
INTEGRABLE_SUBINTERVALS_IMP_MEASURABLE
INTEGRABLE_SUBINTERVALS_IMP_REAL_MEASURABLE
INTEGRABLE_UNIFORM_LIMIT
INTEGRABLE_VSUM
INTEGRAL_0
INTEGRAL_ADD
INTEGRAL_CMUL
INTEGRAL_COMBINE
INTEGRAL_COMBINE_DIVISION_BOTTOMUP
INTEGRAL_COMBINE_DIVISION_TOPDOWN
INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP
INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN
INTEGRAL_COMPONENT
INTEGRAL_COMPONENT_LBOUND
INTEGRAL_COMPONENT_LE
INTEGRAL_COMPONENT_POS
INTEGRAL_COMPONENT_UBOUND
INTEGRAL_CONST
INTEGRAL_DIFF
INTEGRAL_DROP_LE
INTEGRAL_DROP_LE_MEASURABLE
INTEGRAL_DROP_POS
INTEGRAL_EMPTY
INTEGRAL_EQ
INTEGRAL_EQ_0
INTEGRAL_EQ_HAS_INTEGRAL
INTEGRAL_HAS_VECTOR_DERIVATIVE
INTEGRAL_INTERVALS_DIFF_INCLUSION_EXCLUSION
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION_LEFT
INTEGRAL_INTERVALS_INCLUSION_EXCLUSION_RIGHT
INTEGRAL_LINEAR
INTEGRAL_MEASURE
INTEGRAL_MEASURE_UNIV
INTEGRAL_NEG
INTEGRAL_NORM_BOUND_INTEGRAL
INTEGRAL_NORM_BOUND_INTEGRAL_COMPONENT
INTEGRAL_NULL
INTEGRAL_OPEN_INTERVAL
INTEGRAL_PASTECART_CONST
INTEGRAL_PASTECART_CONTINUOUS
INTEGRAL_REFL
INTEGRAL_REFLECT
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_VSUM
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_COMPLEMENT
INTERIOR_CONVEX_HULL_3
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
INTERS_FACES_FINITE_ALTBOUND
INTERS_FACES_FINITE_BOUND
INTERVAL_BIJ_AFFINE
INTERVAL_BIJ_BIJ
INTERVAL_BISECTION
INTERVAL_BISECTION_STEP
INTERVAL_BOUNDS_EMPTY_1
INTERVAL_BOUNDS_NULL_1
INTERVAL_CASES_1
INTERVAL_CONTAINS_COMPACT_NEIGHBOURHOOD
INTERVAL_DOUBLESPLIT
INTERVAL_EQ_EMPTY
INTERVAL_EQ_EMPTY_1
INTERVAL_IMAGE_AFFINITY_INTERVAL
INTERVAL_IMAGE_STRETCH_INTERVAL
INTERVAL_INTER_HYPERPLANE
INTERVAL_LOWERBOUND
INTERVAL_LOWERBOUND_1
INTERVAL_NE_EMPTY
INTERVAL_NE_EMPTY_1
INTERVAL_OPEN_SUBSET_CLOSED
INTERVAL_REAL_INTERVAL
INTERVAL_SING
INTERVAL_SPLIT
INTERVAL_SUBDIVISION
INTERVAL_SUBSET_IS_INTERVAL
INTERVAL_TRANSLATION
INTERVAL_UPPERBOUND
INTERVAL_UPPERBOUND_1
INTER_INTERIOR_UNIONS_INTERVALS
INTER_INTERVAL
INTER_INTERVAL_1
INTER_INTERVAL_MIXED_EQ_EMPTY
INTER_SEGMENT
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
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
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_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_CONVEX_HULL_EXCHANGE
IN_CONVEX_HULL_EXCHANGE_UNIQUE
IN_CONVEX_HULL_LINEAR_IMAGE
IN_CONVEX_SET
IN_DIMINDEX_SWAP
IN_DIRECTION
IN_EPIGRAPH
IN_FROM
IN_FRONTIER_CONVEX_HULL
IN_IMAGE_DROPOUT
IN_IMAGE_LIFT_DROP
IN_INTERIOR
IN_INTERIOR_CBALL
IN_INTERIOR_CLOSURE_CONVEX_SEGMENT
IN_INTERIOR_CLOSURE_CONVEX_SHRINK
IN_INTERIOR_CONVEX_SHRINK
IN_INTERIOR_LINEAR_IMAGE
IN_INTERVAL
IN_INTERVAL_1
IN_INTERVAL_INTERVAL_BIJ
IN_INTERVAL_REFLECT
IN_OPEN_SEGMENT
IN_OPEN_SEGMENT_ALT
IN_PATH_IMAGE_PARTCIRCLEPATH
IN_REAL_INTERVAL
IN_REAL_INTERVAL_REFLECT
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_SEGMENT
IN_SEGMENT_COMPONENT
IN_SEGMENT_CX
IN_SEGMENT_CX_GEN
IN_SLICE
IN_SPAN_DELETE
IN_SPAN_IMAGE_BASIS
IN_SPAN_INSERT
IN_SPHERE
IN_SPHERE_0
IRRATIONAL_APPROXIMATION
ISOLATED_ZEROS
ISOMETRIES_SUBSPACES
ISOMETRY_IMP_AFFINITY
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
ISTOPLOGY_SUBTOPOLOGY
ISTOPOLOGY_OPEN_IN
IS_AFFINE_HULL
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_REALINTERVAL_CONNECTED
IS_REALINTERVAL_CONTINUOUS_IMAGE
IS_REALINTERVAL_CONVEX
IS_REALINTERVAL_CONVEX_COMPLEX
IS_REALINTERVAL_EMPTY
IS_REALINTERVAL_INTERVAL
IS_REALINTERVAL_IS_INTERVAL
IS_REALINTERVAL_UNION
IS_REALINTERVAL_UNIV
IS_REAL_INTERVAL_CASES
ITERATE_AND
ITERATE_NONZERO_IMAGE_LEMMA
ITERATE_SOME
IVT_DECREASING_COMPONENT_1
IVT_DECREASING_COMPONENT_ON_1
IVT_DECREASING_IM
IVT_DECREASING_RE
IVT_INCREASING_COMPONENT_1
IVT_INCREASING_COMPONENT_ON_1
IVT_INCREASING_IM
IVT_INCREASING_RE
ii
in_direction
independent
indicator
infnorm
infsum
inner
inside
integrable_on
integral
interior
interval
interval_bij
interval_lowerbound
interval_upperbound
invertible
is_interval
is_realinterval
is_sphere
istopology