HOL html

Files Index

Theorems Index

E (theorems)

EDELSTEIN_FIX
EDGES_LINEAR_IMAGE
EDGES_TRANSLATION
EDGE_OF_IMP_SUBSET
EDGE_OF_LINEAR_IMAGE
EDGE_OF_TRANSLATION_EQ
EGCD
EGCD_GCD
EGCD_INVARIANT
EGOROV
EL
ELEMENTARY_BOUNDED
ELEMENTARY_COMPACT
ELEMENTARY_EMPTY
ELEMENTARY_INTER
ELEMENTARY_INTERS
ELEMENTARY_INTERVAL
ELEMENTARY_SUBSET_INTERVAL
ELEMENTARY_UNION
ELEMENTARY_UNIONS_INTERVALS
ELEMENTARY_UNION_INTERVAL
ELEMENTARY_UNION_INTERVAL_STRONG
ELEMENTS_PAIR_UP
ELEMENT_IN_LEVEL
EL_APPEND
EL_CONS
EL_MAP
EL_PDI_AT_ZERO
EL_PDI_AT_ZERO2
EL_POLY_DIFF
EL_PRE
EL_REPLICATE
EL_SUC
EL_TL
EMPTY
EMPTY_AS_INTERVAL
EMPTY_AS_REAL_INTERVAL
EMPTY_DELETE
EMPTY_DIFF
EMPTY_DIVISION_OF
EMPTY_EXISTS
EMPTY_EXPOSED_FACE_OF
EMPTY_FACE_OF
EMPTY_GSPEC
EMPTY_INTERIOR_AFFINE_HULL
EMPTY_INTERIOR_CONVEX_HULL
EMPTY_INTERIOR_FINITE
EMPTY_INTERIOR_LOWDIM
EMPTY_INTERIOR_SUBSET_HYPERPLANE
EMPTY_IS_FINITE
EMPTY_NOT_EXISTS
EMPTY_NOT_UNIV
EMPTY_SET
EMPTY_SUBSET
EMPTY_UNION
EMPTY_UNIONS
ENDPOINTS_SHIFTPATH
ENDS_IN_HALFLINE
ENDS_IN_INTERVAL
ENDS_IN_REAL_INTERVAL
ENDS_IN_REAL_SEGMENT
ENDS_IN_SEGMENT
ENDS_IN_UNIT_INTERVAL
ENDS_NOT_IN_SEGMENT
ENR
ENR_ANR
ENR_BALL
ENR_BOUNDED
ENR_CBALL
ENR_CLOSED_UNION
ENR_CLOSED_UNION_LOCAL
ENR_COMPONENT_ENR
ENR_CONNECTED_COMPONENT_ENR
ENR_CONVEX_CLOSED
ENR_DELETE
ENR_EMPTY
ENR_FINITE_UNIONS_CONVEX_CLOSED
ENR_FROM_UNION_AND_INTER
ENR_FROM_UNION_AND_INTER_GEN
ENR_IMP_ABSOLUTE_NEIGHBOURHOOD_RETRACT
ENR_IMP_ABSOLUTE_NEIGHBOURHOOD_RETRACT_UNIV
ENR_IMP_ANR
ENR_IMP_LOCALLY_COMPACT
ENR_IMP_LOCALLY_CONNECTED
ENR_IMP_LOCALLY_PATH_CONNECTED
ENR_INSERT
ENR_INTERIOR
ENR_INTERVAL
ENR_LINEAR_IMAGE_EQ
ENR_NEIGHBORHOOD_RETRACT
ENR_OPEN_IN
ENR_PATH_COMPONENT_ENR
ENR_PATH_IMAGE_SIMPLE_PATH
ENR_PCROSS
ENR_PCROSS_EQ
ENR_RELATIVE_FRONTIER_CONVEX
ENR_RELATIVE_INTERIOR
ENR_RETRACT_OF_ENR
ENR_SIMPLICIAL_COMPLEX
ENR_SING
ENR_SPHERE
ENR_TRANSLATION
ENR_TRIANGULATION
ENR_UNIV
ENSURES_cor1
ENSURES_cor2
ENSURES_cor3
ENSURES_cor4
ENSURES_cor5
ENSURES_cor6
ENSURES_cor7
ENSURES_thm0
ENSURES_thm1
ENSURES_thm2
ENSURES_thm3
ENSURES_thm4
ENSURES_thm5
ENUMERATION_LEMMA
EPSILON_DELTA_MINIMAL
EQUATION_HAS_TYPE_BOOL
EQUIINTEGRABLE_ADD
EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS
EQUIINTEGRABLE_CMUL
EQUIINTEGRABLE_DIVISION
EQUIINTEGRABLE_EQ
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE
EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT
EQUIINTEGRABLE_LIMIT
EQUIINTEGRABLE_NEG
EQUIINTEGRABLE_ON_NULL
EQUIINTEGRABLE_ON_SING
EQUIINTEGRABLE_ON_SPLIT
EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS
EQUIINTEGRABLE_REFLECT
EQUIINTEGRABLE_SUB
EQUIINTEGRABLE_SUBSET
EQUIINTEGRABLE_SUM
EQUIINTEGRABLE_UNIFORM_LIMIT
EQUIINTEGRABLE_UNION
EQUILATERAL_TRIANGLE_ALGEBRAIC
EQUIVALENCE_UNIFORM_PARTITION
EQUIVALENCE_UNIFORM_PARTITION_RESTRICT
EQ_ADD_LCANCEL
EQ_ADD_LCANCEL_0
EQ_ADD_RCANCEL
EQ_ADD_RCANCEL_0
EQ_ANTISYM
EQ_BALLS
EQ_C
EQ_CLAUSES
EQ_C_BIJECTIONS
EQ_EMPTY
EQ_EQ
EQ_EQ_IMP_DISJ_EQ
EQ_EXP
EQ_EXPAND
EQ_EXT
EQ_F
EQ_HOMOL
EQ_HOMOP
EQ_IMP_CONG
EQ_IMP_LE
EQ_INTERVAL
EQ_INTERVAL_1
EQ_MP_correct
EQ_MULT_LCANCEL
EQ_MULT_RCANCEL
EQ_PRIMEPOW
EQ_PRIME_EXP
EQ_REFL
EQ_SPAN_INSERT_EQ
EQ_SUMS_LCANCEL
EQ_SUMS_RCANCEL
EQ_SYM
EQ_SYM_EQ
EQ_T
EQ_TRANS
EQ_UNIV
ERDOS_SZEKERES
ETA_THM
EUCLID
EUCLIDEAN_SPACE_INFINITE
EUCLID_BOUND
EULER
EULERIAN_FINITE
EULERIAN_ODD
EULERIAN_ODD_LEMMA
EULER_CHARACTERISTIC
EULER_CHARACTERISTIC_CELL
EULER_CHARACTERISTIC_CELLCOMPLEX_UNION
EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS
EULER_CHARACTERISTIC_CELL_UNIONS
EULER_CHARACTERISTIC_EMPTY
EULER_CHARACTERISTIC_INCLUSION_EXCLUSION
EULER_CHARACTERSTIC_INVARIANT
EULER_CHARACTERSTIC_LEMMA
EULER_CRITERION
EULER_HAS_INTEGRAL_CGAMMA
EULER_HAS_REAL_INTEGRAL_GAMMA
EULER_INTEGRABLE
EULER_INTEGRAL
EULER_MASCHERONI
EULER_MASCHERONI_APPROX_32
EULER_ORIGINAL_HAS_INTEGRAL_CGAMMA
EULER_ORIGINAL_HAS_REAL_INTEGRAL_GAMMA
EULER_ORIGINAL_INTEGRABLE
EULER_ORIGINAL_INTEGRAL
EULER_ORIGINAL_REAL_INTEGRABLE
EULER_ORIGINAL_REAL_INTEGRAL
EULER_PARTITION_THEOREM
EULER_POINCARE_FULL
EULER_POINCARE_LEMMA
EULER_POINCARE_SPECIAL
EULER_POLYHEDRAL_CONE
EULER_PRODUCT
EULER_PRODUCT_LEMMA
EULER_PRODUCT_MULTIPLY
EULER_REAL_INTEGRABLE
EULER_REAL_INTEGRAL
EULER_RELATION
EULER_ROTATION_THEOREM
EULER_ROTOINVERSION_THEOREM
EVEN
EVEN2
EVENPERM_COMPOSE
EVENPERM_I
EVENPERM_INVERSE
EVENPERM_SWAP
EVENPERM_UNIQUE
EVENTUALLY_AND
EVENTUALLY_AT
EVENTUALLY_ATREAL
EVENTUALLY_AT_INFINITY
EVENTUALLY_AT_INFINITY_POS
EVENTUALLY_AT_NEGINFINITY
EVENTUALLY_AT_POSINFINITY
EVENTUALLY_FALSE
EVENTUALLY_FORALL
EVENTUALLY_HAPPENS
EVENTUALLY_MONO
EVENTUALLY_MP
EVENTUALLY_SEQUENTIALLY
EVENTUALLY_TRUE
EVENTUALLY_WITHIN
EVENTUALLY_WITHINREAL
EVENTUALLY_WITHINREAL_LE
EVENTUALLY_WITHIN_INTERIOR
EVENTUALLY_WITHIN_LE
EVEN_ADD
EVEN_AND_ODD
EVEN_CONS
EVEN_DIV
EVEN_DIV2
EVEN_DIV_LEM
EVEN_DOUBLE
EVEN_EXISTS
EVEN_EXISTS_LEMMA
EVEN_EXP
EVEN_MOD
EVEN_MOD_2
EVEN_MULT
EVEN_NSUM
EVEN_ODD
EVEN_ODD_DECOMP
EVEN_ODD_DECOMPOSITION
EVEN_ODD_POW
EVEN_OR_ODD
EVEN_PHI
EVEN_PHI_EQ
EVEN_POLY_DIFF
EVEN_SQUARE
EVEN_SQUARE_MOD4
EVEN_SUB
EX
EXAMPLE
EXAMPLE_1
EXAMPLE_10
EXAMPLE_2
EXAMPLE_4
EXAMPLE_5
EXAMPLE_7
EXAMPLE_9
EXAMPLE_FACTORIAL
EXCHANGE_LEMMA
EXCLUDED_MIDDLE
EXISTS_ARC_PSUBSET_SIMPLE_PATH
EXISTS_BOOL_THM
EXISTS_CNJ
EXISTS_COMPLEX
EXISTS_COMPLEX'
EXISTS_COMPLEX_ROOT
EXISTS_COMPLEX_ROOT_NONTRIVIAL
EXISTS_COMPONENT_SUPERSET
EXISTS_COUNTABLE_SUBSET_IMAGE
EXISTS_CURRY
EXISTS_DEST_PLANE
EXISTS_DIFF
EXISTS_DOUBLE_ARC
EXISTS_DROP
EXISTS_DROP_FUN
EXISTS_DROP_IMAGE
EXISTS_EX
EXISTS_FINITE_SUBSET_IMAGE
EXISTS_IN_CLAUSES
EXISTS_IN_GSPEC
EXISTS_IN_IMAGE
EXISTS_IN_INSERT
EXISTS_IN_PCROSS
EXISTS_IN_UNION
EXISTS_IN_UNIONS
EXISTS_LE_def
EXISTS_LIFT
EXISTS_LIFT_FUN
EXISTS_LIFT_IMAGE
EXISTS_LINE
EXISTS_LT_def
EXISTS_MOD_EQ
EXISTS_MOD_IMP
EXISTS_MULTIPLE_THM
EXISTS_MULTIPLE_THM_1
EXISTS_NEG
EXISTS_NOT_THM
EXISTS_ONE_REP
EXISTS_OPTION
EXISTS_OR_THM
EXISTS_PAIRED_THM
EXISTS_PAIR_THM
EXISTS_PASTECART
EXISTS_PATH_SUBPATH_TO_FRONTIER
EXISTS_PATH_SUBPATH_TO_FRONTIER_CLOSED
EXISTS_POINT
EXISTS_REAL
EXISTS_REFL
EXISTS_SIMP
EXISTS_SUBARC_OF_ARC_NOENDS
EXISTS_SUBPATH_OF_ARC_NOENDS
EXISTS_SUBPATH_OF_PATH
EXISTS_SUBSET_IMAGE
EXISTS_SUBSET_UNION
EXISTS_SUM_THM
EXISTS_SWAP
EXISTS_THM
EXISTS_TRIPLED_THM
EXISTS_UNCURRY
EXISTS_UNIQUE
EXISTS_UNIQUE_ALT
EXISTS_UNIQUE_REFL
EXISTS_UNIQUE_THM
EXISTS_UNPAIR_THM
EXISTS_VECTOR_1
EXISTS_VECTOR_2
EXISTS_VECTOR_3
EXISTS_VECTOR_4
EXIST_TRANSITION
EXIST_TRANSITION_thm1
EXIST_TRANSITION_thm10
EXIST_TRANSITION_thm11
EXIST_TRANSITION_thm12
EXIST_TRANSITION_thm12a
EXIST_TRANSITION_thm12b
EXIST_TRANSITION_thm2
EXIST_TRANSITION_thm3
EXIST_TRANSITION_thm4
EXIST_TRANSITION_thm5
EXIST_TRANSITION_thm6
EXIST_TRANSITION_thm7
EXIST_TRANSITION_thm8
EXIST_TRANSITION_thm9
EXP
EXPAND_CLOSED_OPEN_INTERVAL
EXPLICIT_SUBSET_INTERIOR_CONVEX_HULL
EXPLICIT_SUBSET_INTERIOR_CONVEX_HULL_MINIMAL
EXPLICIT_SUBSET_RELATIVE_INTERIOR_CONVEX_HULL
EXPLICIT_SUBSET_RELATIVE_INTERIOR_CONVEX_HULL_MINIMAL
EXPOSED_FACE_OF
EXPOSED_FACE_OF_INTER
EXPOSED_FACE_OF_INTERS
EXPOSED_FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE
EXPOSED_FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE
EXPOSED_FACE_OF_LINEAR_IMAGE
EXPOSED_FACE_OF_PARALLEL
EXPOSED_FACE_OF_POLYHEDRON
EXPOSED_FACE_OF_REFL
EXPOSED_FACE_OF_REFL_EQ
EXPOSED_FACE_OF_SUMS
EXPOSED_FACE_OF_TRANSLATION_EQ
EXPOSED_POINT_OF_FURTHEST_POINT
EXPOSED_POINT_OF_INTER_SUPPORTING_HYPERPLANE_GE
EXPOSED_POINT_OF_INTER_SUPPORTING_HYPERPLANE_LE
EXP_0
EXP_1
EXP_10_CONG_3
EXP_2
EXP_4
EXP_ADD
EXP_EQ_0
EXP_EQ_1
EXP_EXP
EXP_ITER
EXP_LE_REFL
EXP_LIMIT
EXP_LN
EXP_LOG
EXP_LT_0
EXP_MONO_EQ
EXP_MONO_EQ_SUC
EXP_MONO_LE
EXP_MONO_LE_IMP
EXP_MONO_LE_SUC
EXP_MONO_LT
EXP_MONO_LT_IMP
EXP_MONO_LT_SUC
EXP_MULT
EXP_MULT_EXISTS
EXP_NEG_X_DIFF
EXP_ONE
EXP_ZERO
EXPinj
EXTEND_FL
EXTEND_INSEG
EXTEND_LINSEG
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_GEN
EXTEND_MAP_AFFINE_TO_SPHERE_COFINITE_SIMPLE
EXTEND_MAP_SPHERE_TO_SPHERE
EXTEND_MAP_SPHERE_TO_SPHERE_COFINITE
EXTEND_MAP_SPHERE_TO_SPHERE_COFINITE_GEN
EXTEND_MAP_SPHERE_TO_SPHERE_GEN
EXTEND_MAP_UNIV_TO_SPHERE_COFINITE
EXTEND_MAP_UNIV_TO_SPHERE_NO_BOUNDED_COMPONENT
EXTEND_TO_AFFINE_BASIS
EXTENSION
EXTENSIONALITY_LEVEL
EXTENSIONALITY_NONEMPTY
EXTENSION_FROM_CLOPEN
EXTENSION_FROM_COMPONENT
EXTENSION_INTO_AR
EXTENSION_INTO_AR_LOCAL
EXTREME_POINTS_OF_CONVEX_HULL
EXTREME_POINTS_OF_CONVEX_HULL_EQ
EXTREME_POINTS_OF_LINEAR_IMAGE
EXTREME_POINTS_OF_TRANSLATION
EXTREME_POINT_EXISTS_CONVEX
EXTREME_POINT_NOT_IN_INTERIOR
EXTREME_POINT_NOT_IN_RELATIVE_INTERIOR
EXTREME_POINT_OF_CONIC
EXTREME_POINT_OF_CONVEX_HULL
EXTREME_POINT_OF_CONVEX_HULL_2
EXTREME_POINT_OF_CONVEX_HULL_AFFINE_INDEPENDENT
EXTREME_POINT_OF_CONVEX_HULL_CONVEX_INDEPENDENT
EXTREME_POINT_OF_CONVEX_HULL_EQ
EXTREME_POINT_OF_CONVEX_HULL_INSERT
EXTREME_POINT_OF_CONVEX_HULL_INSERT_EQ
EXTREME_POINT_OF_EMPTY
EXTREME_POINT_OF_FACE
EXTREME_POINT_OF_INTER
EXTREME_POINT_OF_INTER_SUPPORTING_HYPERPLANE_GE
EXTREME_POINT_OF_INTER_SUPPORTING_HYPERPLANE_LE
EXTREME_POINT_OF_LINEAR_IMAGE
EXTREME_POINT_OF_MIDPOINT
EXTREME_POINT_OF_SEGMENT
EXTREME_POINT_OF_SING
EXTREME_POINT_OF_STILLCONVEX
EXTREME_POINT_OF_TRANSLATION_EQ
EX_IMP
EX_MAP
EX_MEM
E_APPROX_32
E_DEF
E_POW_N
E_TRANSCENDENTAL_EQUIV
edge_cell
edge_euclid2
edge_h
edge_inter
edge_midend
edge_of
edge_subset_ctop
edge_v
edgec_convex
edges
egcd
element
elemma0
ellipsoid
empty_closed
empty_mat
endpoint_closure
endpoint_cls
endpoint_criterion
endpoint_edge
endpoint_even
endpoint_lemma
endpoint_lemma_big_fst
endpoint_lemma_big_snd
endpoint_lemma_mid_fst
endpoint_lemma_small_fst
endpoint_lemma_summary
endpoint_lemma_upper_left
endpoint_lemma_upper_right
endpoint_psegment
endpoint_size2
endpoint_sub_rectagon
endpoint_subrectagon
epigraph
eps_hyper_inj
eps_hyper_ne
eps_hyper_scale
eps_hyper_scale_perp
eps_hyper_translate
eps_hyper_translate_perp
eps_translate
eq_c
eq_eq_false_thm
eq_exchange
eq_ge_thm
eq_gt_thm
eq_le_thm
eq_lem
eq_lt_thm
eq_pair_exchange
eq_sing
eq_sing_sym
eq_sym
eq_sym_rule
eq_trans
eq_trans_imp
eq_trans_rule
equation
equiintegrable_on
equivalence_relation
erica13
erica14
erica8
eth
euclid0_point
euclid1_abs
euclid1_dirac
euclid2_d0
euclid2_e12
euclid2_point
euclid_add_assoc
euclid_add_cancel
euclid_add_closure
euclid_add_comm
euclid_ball_cube
euclid_cancel1
euclid_diff_par_cell
euclid_dirac
euclid_eq_minus
euclid_euclid0
euclid_ldistrib
euclid_lzero
euclid_minus0
euclid_minus_scale
euclid_n_convex
euclid_neg_closure
euclid_neg_sum
euclid_plus_pair
euclid_point
euclid_rdistrib
euclid_rzero
euclid_scale0
euclid_scale_act
euclid_scale_bij
euclid_scale_cancel
euclid_scale_closure
euclid_scale_cont
euclid_scale_homeo
euclid_scale_inv
euclid_scale_one
euclid_scale_rinv
euclid_scale_simple_arc_ver2
euclid_segment
euclid_sub_closure
euclid_updim
euclid_xy
euclidean
euclidean_add_closure
euclidean_neg_closure
euclidean_scale_closure
euclidean_sub_closure
euclideanreal
euler_characteristic
euler_mascheroni
eval
even_card_even
even_cell_h_edge
even_cell_point
even_cell_squ
even_cell_v_edge
even_delete
even_num_lower_union
evenperm
eventually
exI
ex_falso
exiff
eximp
exists_function_unpair
exists_imp
exists_intro
exp
exp_INDUCT,exp_RECURSION
exp_gt1
expand_prod_le
expand_prod_lt
exposed_face_of
expression_INDUCT,expression_RECURSION
extreme_point_of