HOL html

Files Index

Theorems Index

E (theorems)

EACH_ELM_PRESERVED_IMP_ALL
EACH_ELM_PRESERVED_IMP_ALLL
EAPGLE
EAR_DELTA_X4
EAR_DIH1_DELTA_0
EAR_SOL_NN
EAR_STABLE_SYSTEM
EAR_TRI_STABLE_SYSTEM
ECAU_aff_ge
ECNT
ECSEVNC
ECTC
EDGES0_FAN
EDGES0_SUBSET_FAN
EDGEX_PAIR
EDGEX_SUBSET_MCELL
EDGE_4I2_LE_2H0
EDGE_DOT_LE_NORM
EDGE_EQ_2_4I2
EDGE_EQ_2_4I2_1
EDGE_EQ_2_4I2_2
EDGE_EQ_2_4I2_3
EDGE_EQ_2_4I2_ALL
EDGE_FINITE
EDGE_FORM_IN_LOCAL_FAN
EDGE_HYPERMAP_OF_FAN
EDGE_IMP_K2
EDGE_IMP_K23
EDGE_IN_E_SY
EDGE_IN_F_SY
EDGE_IN_LOCAL_FAN_DET_RHO_NODE
EDGE_LE_2RAD
EDGE_LIST_ALL
EDGE_MAP_SYM_0
EDGE_MCELL_EL
EDGE_NOT_EMPTY
EDGE_NOT_INTER_WITH_WEDGE
EDGE_OF_FACET_EDGE
EDGE_OF_FACET_OF
EDGE_OF_SIZE_2
EDGE_PAIR_pr23
EDGE_POWER_MAP_SYM_0
EDGE_SUBSET_DART1_OF_FAN
EDGE_pr23
ED_MA_O_NO_MA_EQ_INV_FA
EE
EE_EXPAND_BB_VV
EE_FST_Y_EQ_SET_SET_SNDY
EE_OF_HYP_HAS_ORDERS
EE_OF_HYP_IDE_FST_SND_EQ
EE_OF_HYP_PERMUTES_DARTS
EE_SING_SING
EE_SUBSET_UNIONS_E
EE_SYM_0
EE_UNION
EE_elim
EE_vv
EGHNAVX
EGHNAVX1_ALT
EGHNAVX_COLL_SCS
EGHNAVX_SCS
EJRCFJD
EJRCFJD_ALT
EJRCFJD_ALT2
ELEMENT1_SYM_0
ELEMENT2_SYM_0
ELMS_OF_HYPERMAP_HYP
EL_0
EL_1
EL_2
EL_3
EL_BUTLAST
EL_CC_UH
EL_DROP
EL_EQ_IMP_EQ
EL_EXPLICIT
EL_INDEX
EL_LEFT_ACTION_LIST
EL_LIST_PAIRS
EL_LIST_PAIRS2
EL_L_SEQ
EL_REVERSE
EL_REVERSE_TABLE
EL_SHIFT_LEFT
EL_SHIFT_RIGHT
EL_TABLE
EL_TRUNCATE_SIMPLEX
EL_ZIP
EMNWUUS1
EMNWUUS2
EMPTY_EQ_SYM_0
EMPTY_EXISTS
EMPTY_NOT_EXISTS_IN
END_POINT_ADD_IN_AFF2
EPS_TO_INTERVAL
EQUATE_CONEFS_POLINOMIAL_POW2
EQUI_FF_SYM_0
EQ_0_0
EQ_0_NUM
EQ_B0_0
EQ_CARD_FACE_FAN_AND_FANADD
EQ_DIAGONAL_MIN
EQ_DIAG_STAB_4I1_02
EQ_DIAG_STAB_5I1_02
EQ_DIAG_STAB_5I2_02
EQ_DIAG_STAB_6I1_02
EQ_DIAG_STAB_6I1_03
EQ_EDGE_E_SY
EQ_EDGE_E_SY1
EQ_IMP_COPLANAR
EQ_PAIR_4
EQ_PAIR_IMP_EQ_4_FAN
EQ_POW2_COND
EQ_SET_PAIR_SYM_0
EQ_SET_THM
EQ_SPAN_INSERT_EQ
EQ_SQRT_POW2_EQ
EQ_SUB_DIST_POW2_IMP_IDENTIFIED
EQ_SUC_K_SUB
EQ_SUC_K_SUB3
EQ_W_L_IN_BBS
ESTD
ESTD_fan0
ESTD_fan1
ESTD_fan2
ESTD_fan6
ESTD_fan7
ETA_X_SYM
ETA_X_SYMM
ETA_Y_2
ETA_Y_4_POINTS_INEQ
ETA_Y_BOUNDS
ETA_Y_LEMMA
ETA_Y_LEMMA_ALT
ETA_Y_LE_IMP_LT
ETA_Y_LE_IMP_LT_ALL
ETA_Y_LT_SQRT2
ETA_Y_POS_LE
ETA_Y_POS_LE_ALT
ETA_Y_POW2_EQ
ETA_Y_SQRT8_2_251
ETA_Y_SYM
ETA_Y_SYYM
EUCLIDEAN_SPACE_INFINITE
EULER_ANGLE_SUM_rescal
EULER_FORMULA_RESCALE
EULER_TRIANGLE
EULER_TRIANGLE_REAL_INTERVAL
EUSOTYP2_general
EUSOTYP_general
EUSOTYP_simple
EVENTUALLY_RADIAL_AFF_GE
EVENTUALLY_RADIAL_CONVEX_HULL_4_sub1
EVENTUALLY_RADIAL_EMPTY
EVENTUALLY_RADIAL_INTER
EVENTUALLY_RADIAL_NOT_IN_CLOSED_SET
EVENTUALLY_RADIAL_RCONE_GE_ABC_A
EVENTUALLY_RADIAL_RCONE_GE_ABC_B
EVENTUALLY_RADIAL_UNNORM
EVEN_B0
EVEN_SUC_F
EVEN_SUC_T
EVEN_ZERO
EWYBJUA
EXCHANGE_LEMMA
EXISTS_AND_IMP
EXISTS_BIJ_SQUARE
EXISTS_DIA
EXISTS_DROP
EXISTS_DROP_FUN
EXISTS_EDGE_AT_VERTICES
EXISTS_EDGE_POLYTOPE
EXISTS_EDGE_POLYTOPE1
EXISTS_INTERSECTION_PROPERPLY
EXISTS_INVERSE_OF_V
EXISTS_IN_UNIT_INTERVAL
EXISTS_LIFT
EXISTS_LIFT_FUN
EXISTS_MAX_ELEMENT
EXISTS_MIN_IN_ORDERED_FINITE_SET
EXISTS_M_POLYHEDRON
EXISTS_OTHOR_VECTOR_DIFFF_VEC0
EXISTS_POINT_DART_OF_HYP
EXISTS_POINT_IN_FCHANGED
EXISTS_PROJECTING_POINT
EXISTS_PROJECTING_POINT2
EXISTS_QY_CARD5
EXISTS_SMALLEST_ELMS
EXISTS_SMALL_LE_CONST
EXISTS_SMALL_LE_CONST_ADD
EXISTS_SMALL_LE_CONST_V1
EXISTS_SMALL_LT_CONST
EXISTS_SMALL_LT_CONST_ADD
EXISTS_SMALL_LT_CONST_V1
EXISTS_STEPS_FOR_FOLLOWING_POINTS
EXISTS_TRIPLED_THM
EXISTS_TRIPLE_THM
EXISTS_UNIQUE_TRIPLED_THM
EXISTS_UNIT_OTHOR_VECTOR
EXISTS_VECTOR_1
EXISTS_VECTOR_2
EXISTS_VECTOR_3
EXIS_SMALLEST_WITH_AZIM_ORD
EXI_THIRD_PO
EXPAND_DIAG_4
EXPAND_DIAG_4V
EXPAND_DIAG_4_DIST
EXPAND_EDGE_POLYTOPE
EXPAND_PERIODIC
EXPAND_SET_THREE_ELEMENTS
EXPAND_SET_TWO_ELEMENTS
EXPAND_STAB_DIAG
EXPAND_STAB_DIAG_4
EXPAND_STAB_DIAG_4I1
EXPAND_STAB_DIAG_4I3
EXPAND_STAB_DIAG_4M2
EXPAND_STAB_DIAG_4M3
EXPAND_STAB_DIAG_4M4
EXPAND_STAB_DIAG_4M5
EXPAND_STAB_DIAG_4M6
EXPAND_STAB_DIAG_4M7
EXPAND_STAB_DIAG_4M8
EXPAND_STAB_DIAG_5
EXPAND_STAB_DIAG_5I1
EXPAND_STAB_DIAG_5I2
EXPAND_STAB_DIAG_5I3
EXPAND_STAB_DIAG_5M1
EXPAND_STAB_DIAG_5M3
EXP_INV_lemma
EXTENSION_SIGMA_FAN_EQ_RES
EXTENSION_SIGMA_FAN_INJECTIVE
EXTREMAL_SCS_4M6
EYFCXPP
EYYPQDW
EYYPQDW2
EYYPQDW3
EYYPQDW_CONTINUOUS_AT_V
EYYPQDW_CONTINUOUS_AT_X
EYYPQDW_CONTINUOUS_LIFT_DIST
EYYPQDW_CONTINUOUS_LIFT_DIST_ADD
EYYPQDW_COPLANAR
EYYPQDW_NORMV3
EYYPQDW_NORM_V3_V1
EYYPQDW_SCALAR_POS
EYYPQDW_V3_DEFOR_INCREASING_IN_ANGLE
E_DEFORMATION_V3_DEFOR
E_DEFORMATION_V3_DEFOR_V5
E_DEFORMATION_WW_DEFOR
E_FAN_PAIR_EXT
E_FAN_PAIR_EXT_EXPLICIT
E_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN
E_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN
E_HAS_NO_FIXED_POINTS_IN_D1
E_LIST_EXT_INVOLUTION
E_LIST_EXT_PERMUTES_DARTS
E_N_F_DEGENERATE_CASE
E_N_F_EQ_I
E_N_F_ID
E_N_F_IN_DART1_OF_FAN
E_PRIME_EQ_E_vv
E_PRIME_SUBSET_E
E_SY
e1_cross_e2_dot_e3_fan
e1_fan
e1_is_normal_fan
e1_orthogonal_e2_fan
e1_orthogonal_e3_fan
e2_fan
e2_is_normal_fan
e2_orthogonal_e3_fan
e3_fan
e3_is_normal_fan
e3_mul_dist_fan
e_fan
e_fan_no_fix_point
e_fan_pair
e_fan_pair_ext
e_fan_permutes
e_hyp_of_fan
e_list
e_list_ext
e_of_hyp
e_plane
e_prime
e_std
ear_acute
ear_sy
edge
edge2_126_x
edge2_135_x
edge2_234_x
edge2_flatD_sym
edge2_flatD_x1
edge2_flatD_x1_continuous
edge2_flatD_x1_delta_lemma2
edge2_flatD_x1_delta_lemma3
edge2_flatD_x1_expanded
edge2_flatD_x1_quadratic_root_plus
edge2_flatD_x1_sym_cases
edge2_flatD_x1_works
edgeX
edge_126_x
edge_135_x
edge_CARD
edge_CARD_dart
edge_convolution
edge_cyclic_map_lemma
edge_datum
edge_deform
edge_degenerate_walkup_edge_map
edge_degenerate_walkup_first_eq
edge_degenerate_walkup_second_eq
edge_degenerate_walkup_third_eq
edge_flat
edge_flat2_x
edge_flat2_x_rewrite
edge_flat50_x
edge_flatD_x1
edge_flat_x
edge_lie_different_nodes
edge_map
edge_map_and_darts
edge_map_convolution
edge_map_injective
edge_map_inverse_representation
edge_map_of_fan
edge_map_walkup
edge_nondegenerate
edge_not_in_ds2
edge_path
edge_quadratic
edge_refl
edge_set
edge_slice
edge_walkup
edges_of_facet_of
ee_of_hyp
ee_of_hyp2
ee_of_hyp3
ee_of_hyp_elim
ejr_distinct
ejr_generic
ejr_sum
elements_in_ds2_fan
elements_of_list
elim_power_function
ell_uvx
ell_vx2
ellipsoid
emap
emap_permute
emap_via_choice
empty_3T1
empty_3T2
empty_3T3
empty_3T4
empty_3T5
empty_3T6
empty_3T7
empty_4T1
empty_4T2
empty_4T3
empty_4T4
empty_4T5
empty_5T1
empty_6T1
enclosed
enclosed4_lemma
enclosed_sym
enclosed_sym2
epsilon_hept
epsilon_hex
epsilon_lemma
epsilon_pair
epsilon_pent
epsilon_quad
epsilon_triple
eq0_th
eq3_th
eq4_th
eq5_th
eq6_th
eq_aff_gt_3_fanadd_edge
eq_def_intball
eq_set_aff_gt
eq_set_wdart_fan
eq_th
equality_dart_leads_into
equality_real_fan
equivalence_relation
equivalent_lemma
error_mul_f1
error_mul_f2
estd_non_collinear_lemma
estimate0
estimate1
estimate2
estimate3
eta2_126
eta2_126_eta_x_open
eta2_135
eta2_456
eta2_assum
eta_pos
eta_v
eta_x
eta_x_ineq_lemma
eta_y
eta_y_nn
eulerA_hexall_x
eulerA_x
eulerA_x_pos
eulerA_x_sym
eulerA_x_sym_cases
euler_1flat_x
euler_1flat_x_alt
euler_2flat_x
euler_2flat_x_alt
euler_3flat_x
euler_3flat_x_alt
euler_ap
euler_p
euler_p_eulerA_x
eunion
eus1
eus_cos
evaluation_samsara
eventally_measurable_fanadd
eventually_radial
eventually_radial_norm
eventually_radial_norm_deprecated
ex_fun
ex_set
exceptional
exceptional_face
exceptional_faces
exceptional_faces_set
exist_close1_fan
exist_close_fan
exist_fan
exist_hypermap
exist_lemma
exist_lemma1
exist_loop
exist_stable_system
exist_tri_stable
existence_contour
exists_ballsets_fan
exists_connect_point_in_xfanto_yfan
exists_cross_dot_fully_surrounded1_fan
exists_cross_dot_fully_surrounded1_fan_le
exists_cross_dot_fully_surrounded2_fan
exists_cross_dot_fully_surrounded2_fan_le
exists_cut_in_edge_fan
exists_cut_rcone_fan_with_edge_run_fan
exists_cut_small_edges_fan
exists_cut_small_edges_fan_le
exists_dart_leads_into_edge_eq_topological1_component_fan
exists_dart_leads_into_edge_eq_topological_component_fan
exists_dartset_leads_into_fan
exists_edge_bounded_topological_component_yfan
exists_edge_component_yfan
exists_edge_fully_surround_fan
exists_edge_not_edge_in_face
exists_edge_rw_dart_fan_inter_aff_gt_not_empty_fan
exists_edge_rw_dart_fan_inter_topological_component_not_empty_fan
exists_element_in_half_sapace_fan
exists_eq
exists_esilon_real
exists_face_in_face_set
exists_function_inverse_sigma_fan_alt
exists_in_aff_gt
exists_in_aff_gt_disjoint
exists_inf_element_fix_fan
exists_inverse_in_orbits_sigma_fan
exists_inverse_sigma_fan_alt
exists_leads_into_fan
exists_measure_ball_diff_set_negligible
exists_node_in_face_set
exists_open_not_collinear
exists_point_dart_leads_into_fan
exists_point_in_V
exists_point_in_component_yfan
exists_point_in_dartset_leads_into_fan
exists_point_in_node
exists_point_inside_domain_cone_fan
exists_point_notx_in_xfan
exists_point_notxin_convex_in_xfan
exists_point_small_edges_fan
exists_point_small_edges_not0_fan
exists_rw_dart_inter_aff_gt1_fan
exists_rw_dart_inter_aff_gt_fan
exists_sigma_fan
exists_tranf_fan
exists_vv
exists_vv3
exists_vv_FF
exp_aff_by_dot
exp_aff_ge_by_dot
exp_aff_ge_by_dot_1_1
exp_aff_gt_by_dot
expand_edge_graph_fan
expand_element_in_topological_component_yfan
expand_elements_by_azim_fan
expand_prod_le
expand_prod_lt
expand_set_edge_fan
expand_unions
expand_xfan_eq_aff_gt_aff_ge
expansion1_convex_fan
expansion_convex_fan
ext_dart
extended_dart
extension_in_aff_2_2_fan
extension_sigma_fan
exterior_contour
extra_assum_derived_form