HOL html

Files Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _
Theorems Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _

A (theorems)

AAA_LEMMA
AAUHTVE
ABS_BUMP
ABS_DROP
ABS_LE_1_IMP_SIN_ACS
ABS_LE_BOUNDS
ABS_LT_EPSI
ABS_NOT_EQ_NORM_MUL
ABS_NUM
ABS_NUM_P
ABS_POS
ABS_PROD
ABS_SQUARE
ABS_SQUARE_LE
ABS_TO_INTERVAL
ABS_TRIANGLE
ACR_REFL
ACS_2
ACS_ARCLENGTH
ACS_ATN_ALT
ACS_ROOT32
ADD_0_n
ADD_COMM
ADD_C_UNIV
ADD_NN_ZERO
ADD_NUM
ADD_n_0
ADJOINT_ADJOINT
ADJOINT_CLAUSES
ADJOINT_INJECTIVE
ADJOINT_INJECTIVE_INJECTIVE
ADJOINT_INJECTIVE_INJECTIVE_0
ADJOINT_LINEAR
ADJOINT_MATRIX
ADJOINT_SURJECTIVE
ADJOINT_UNIQUE
ADJOINT_WORKS
AFF2
AFF2_DET_BY_TWO_POINTS
AFF2_ITR_CONV0_IMP_SAME_ENDS
AFF2_VEC0
AFF3_TRANSLATION_IMAGE
AFFINES_INTER_BALL_EQ_IMP_EQ
AFFINE_AFF
AFFINE_AFF_HULL
AFFINE_BIS
AFFINE_BOUNDED_EQ_LOWDIM
AFFINE_BOUNDED_EQ_TRIVIAL
AFFINE_CONTAIN_LINE
AFFINE_DEPENDENT_3_IMP_COLLINEAR
AFFINE_DEPENDENT_EXPLICIT_4
AFFINE_DEPENDENT_KY_LEMMA1
AFFINE_HULL_1
AFFINE_HULL_3
AFFINE_HULL_3_GENERATED
AFFINE_HULL_3_INSERT
AFFINE_HULL_4
AFFINE_HULL_AFFINE_EQ
AFFINE_HULL_CIRCUMCENTER_EQ
AFFINE_HULL_CIRCUMCENTER_PROJECTION
AFFINE_HULL_FINITE
AFFINE_HULL_FINITE_STEP_GEN
AFFINE_HULL_INTERS_BIS
AFFINE_HULL_PROJECTION_DIST_EQ
AFFINE_HULL_PROJECTION_DIST_LE
AFFINE_HULL_PROJECTION_DIST_LT
AFFINE_HULL_PROJECTION_EXISTS
AFFINE_HULL_PROJECTION_SEPARATES
AFFINE_HULL_RADV
AFFINE_HULL_SINGLE
AFFINE_HULL_VORONOI_LIST_SUBSET_INTERS_BIS
AFFINE_IMP_CHI_MSB_0
AFFINE_INDEPENDENT_IMP_INDEPENDENT
AFFINE_INDEPENDENT_OMEGA_LIST_N
AFFINE_SET_GENERARTED2
AFFINE_SET_GEN_BY_TWO_POINTS
AFFINE_SUBSET_KY_LEMMA
AFFINE_VEC0
AFFINITE_HULL_BALL_EQ_UNIV
AFF_2POINTS_INTERPRET
AFF_CONV0_COLL4
AFF_CONV0_INTERSECTION_LEMMA
AFF_CONV0_IN_AFF_LT
AFF_DEPENDENT_AFF_DIM_4
AFF_DEP_COPLANAR
AFF_DIM_3
AFF_DIM_FINITE_UNION_LE
AFF_DIM_INTERIOR_EQ_3
AFF_DIM_LE_2_IMP_COPLANAR
AFF_DIM_LE_LENGTH
AFF_DIM_VORONOI_CLOSED
AFF_DIM_VORONOI_LIST
AFF_GE11_SUB_AFF2
AFF_GE21_SUBSET_AFF22
AFF_GE22
AFF_GE33
AFF_GES_GTS
AFF_GES_LTS
AFF_GE_12
AFF_GE_1_1
AFF_GE_1_10
AFF_GE_1_1_0
AFF_GE_1_2
AFF_GE_1_2_0
AFF_GE_1_3
AFF_GE_2_1
AFF_GE_2_1_0
AFF_GE_2_1_0_DROPOUT_3
AFF_GE_2_1_0_SEMIALGEBRAIC
AFF_GE_2_2
AFF_GE_3_1
AFF_GE_BREAK_KY_LEMMA
AFF_GE_COMMUTATIVE_SYM_0
AFF_GE_EQ
AFF_GE_EQ_AFF_GE_UNION
AFF_GE_INTER_AFF_GT_EQ_EMPTY
AFF_GE_INTER_AFF_LT_IMP_NOT_EQ_COL
AFF_GE_MONO_TRANS
AFF_GE_SCALE_LEMMA
AFF_GE_SUBSET_AFF_GE_UNION
AFF_GE_SUBSET_WEDGE_GE
AFF_GE_SUBSET_XFAN
AFF_GE_TO_AFF_GT2_GE1
AFF_GE_VEC0_SYM_0
AFF_GE_WEDGE_DISJOINTION
AFF_GT22
AFF_GT33
AFF_GT_0_2
AFF_GT_1_1
AFF_GT_1_1_SUBSET_DARTSET_LEADS_INTO_FAN
AFF_GT_1_2
AFF_GT_1_3
AFF_GT_1_3_SUBSET_AFF_GT_1_3
AFF_GT_2_2
AFF_GT_3_1
AFF_GT_AFF_LT_INTERPRET
AFF_GT_COMMUTATIVE_SYM_0
AFF_GT_CUT_XFAN_IMP_EDGE_FAN
AFF_GT_INTER_AFF_SY
AFF_GT_IN_IMP_SUBSET
AFF_GT_LT_INTER_SYM
AFF_GT_MONO
AFF_GT_MONO_TRANS
AFF_GT_RELATIVE_INTERIOR
AFF_GT_SAME_WITH_ENDS
AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN
AFF_GT_SUBSET_DARTSET_LEADS_INTO
AFF_GT_SUBSET_DART_LEADS_INTO_FAN
AFF_GT_SUBSET_FCHANGED
AFF_GT_SUBSET_WEDGE_IMP_VERTEX
AFF_GT_VEC0_SYM_0
AFF_HULL_TWO_POINTS
AFF_INDEPENDENT_SET_OF_LIST_BARV
AFF_INTER_AFF_GT_EQ_EMPTY
AFF_INTER_IMP_COPLANAR
AFF_INTER_SUBSET_INTER_AFF
AFF_IN_TWO_PARTS
AFF_IVS_RHO_NODE_EQQ
AFF_LE_COMMUTATIVE_SYM_0
AFF_LE_CONE
AFF_LE_LT33
AFF_LE_VEC0_SYM_0
AFF_LT21
AFF_LT31
AFF_LT_1_1
AFF_LT_2_1
AFF_LT_COMMUTATIVE_SYM_0
AFF_LT_SUBSET_AFF11
AFF_LT_VEC0_SYM_0
AFF_SUB_PLANE
AFF_XX_CASES
AGBWHRD
AJRIPQN
AJRIPQN_0
ALL2_0'
ALL2_ALL_ZIP
ALLEMI_COLLINEAR
ALL_0'
ALL_ABOUT_COEF_1
ALL_ABOUT_COEF_2
ALL_ABOUT_COEF_3
ALL_DISTINCT
ALL_DISTINCT_ALT
ALL_DISTINCT_APPEND
ALL_DISTINCT_APPEND_SYM
ALL_DISTINCT_FACE
ALL_DISTINCT_FACE_UNIQUE
ALL_DISTINCT_FILTER
ALL_DISTINCT_FIND_FACE
ALL_DISTINCT_FLATTEN
ALL_DISTINCT_IMP_INDEX_UNIQUE
ALL_DISTINCT_IMP_UNIQUE_LIST
ALL_DISTINCT_LIST_PAIRS
ALL_DISTINCT_NODE
ALL_DISTINCT_NUM_PAIR_EMPTY
ALL_DISTINCT_REMOVE_DUPLICATES
ALL_DISTINCT_SHIFT_LEFT
ALL_DISTINCT_SUBLIST_UNIQUE
ALL_DISTINCT_SUM
ALL_EL
ALL_FILTER
ALL_N_ALL2
ALL_N_EL
ALL_N_EMPTY'
ALL_TO_THE_NONPARALLEL_PART
ALL_TO_THE_NONPARALLEL_PART_ALT
AMHFNXP
AMHFNXP_BIJ
AND_FORALL_TAG
ANGLES_ADD_AFF_GE
ANGLE_EQ_ARCV
ANGLE_EQ_DIHV
ANGLE_GT_PI2
ANGLE_SUM_BOUND
ANGLE_SUM_lemma
APPEND_LINEAR_IMAGE
APPEND_TRANSLATION
APPROX_INTERVAL
AQICLXA
AQICLXA_SLICE
ARCV_ADD_AFF_GE
ARCV_BOUNDED
ARCV_BOUNDS
ARCV_DEGENERATE
ARCV_DETER_DIRECTION
ARCV_DIRECTIONS
ARCV_EQ_0
ARCV_EQ_0_ORIGIN
ARCV_EQ_IMP_NORMIZE
ARCV_GT_PI2
ARCV_INEQUALTY
ARCV_ORI_DIRECTIONS
ARCV_PI_OPPOSITE
ARCV_VEC0_ABS
ARCV_VEC0_FORM
ARC_222
ARC_OPPOSITE
ARC_SYM
ARDBZYE
ARG_0_DIV
ARG_CNJ
ARG_DIFF_SUCCESSIBLE_IN_FIRST_PERIOD
ARG_DIV_EQ_SUBSET_HALFLINE
ARG_EQ_SUBSET_HALFLINE
ARG_INV_ALT
ARG_ORDER
ARG_SCALE
ARIKWRQ
ARITH_3_TAC
ARITH_4_TAC
ARITH_5_TAC
ARITH_6_TAC
ASN_HALF
ASSOCD_v39
ASSUME_MIN_DIAG
ASSWPOW
ATAN2_EXISTS
ATAN2_TEMP
ATAN2_TEMP_ALT
ATAN2_TEMP_BREAKDOWN
ATAN2_TEMP_DEF
ATAN2_TEMP_SPEC
ATAN_TEMP_ATN2
ATN2_0_1
ATN2_0_NEG_1
ATN2_30
ATN2_45
ATN2_60
ATN2_90
ATN2_ACS_LEMMA
ATN2_ARCLENGTH
ATN2_ATN
ATN2_ATN_XPOS
ATN2_BREAKDOWN
ATN2_CIRCLE
ATN2_LE_PI2
ATN2_LMUL_EQ
ATN2_POS
ATN2_RNEG
ATN2_ROT_TAN
ATN2_Y_NEG
ATN_INV
ATN_SUM_TABLE
ATN_UPS_X_BREAKDOWN1
AT_FAN
AT_INFINITY_FAN
AUEAHEH
AURSIPD
AUTOMAP_IMP_ALL_ITER_IN
AUTOMAP_IMP_ITER_SET_IS_A_SUBSET
AXJRPNC
AYQJTMD
AZIM_0_WW_DEFOR
AZIM_AND_ARCV_EQ_IMP_PARA
AZIM_ARCV
AZIM_ARG4
AZIM_BASE_SHIFT_LE
AZIM_BASE_SHIFT_LT
AZIM_COMP2_LE
AZIM_COMP2_LT
AZIM_COMPL_EXT
AZIM_COMPL_NEG
AZIM_COMP_LE
AZIM_COMP_LT
AZIM_COND_FOR_COPLANAR
AZIM_CYCLE1_SYM_0
AZIM_CYCLE2_SYM_0
AZIM_CYCLE_BASIC_PROPERTIES
AZIM_CYCLE_EQ
AZIM_CYCLE_EQ1
AZIM_CYCLE_EQ_SIGMA_FAN
AZIM_CYCLE_EQ_SIGMA_FAN_ALT
AZIM_CYCLE_PROPERTIES
AZIM_CYCLE_SING
AZIM_CYCLE_SING_ALT
AZIM_CYCLE_SYM_0
AZIM_CYCLE_TWO_POINT_SET
AZIM_CYCLE_TWO_POINT_SET_ALT
AZIM_CY_FST_Y_IN_FF
AZIM_DART_POS
AZIM_DEFORMATION_GENERIC
AZIM_DEFOR_EDGE1
AZIM_DEFOR_EDGE2
AZIM_DEFOR_EDGE3
AZIM_DIHV_SAME_STRONG
AZIM_EQ_0_GE_ALT2
AZIM_EQ_0_SYM2
AZIM_EQ_DIHV_IN_B_SY
AZIM_EQ_LE_SYM_0
AZIM_EQ_PI_POINT_SYM_0
AZIM_EQ_SYM
AZIM_IN_FAN_EQ_IZIM_E_PRIME
AZIM_IN_FAN_RHOND_IVS_RHOND
AZIM_IN_UPPER_HALFSPACE
AZIM_I_FAN_EQ_AZIM_DART
AZIM_LAST_POINT_IN_RHO_SET
AZIM_LAST_POINT_IN_RHO_SET2
AZIM_LE_PI_EQ_DIHV
AZIM_LE_PI_EQ_DIHV_ALT
AZIM_LE_PI_SYM_0
AZIM_LE_POWER_SIGMA_FAN
AZIM_NEG
AZIM_NEG_FIRST_PI
AZIM_NN
AZIM_PI
AZIM_PI1
AZIM_PI_CONVEX_WEDGE
AZIM_PI_ITER_LOCAL_FAN
AZIM_PI_LEMMA
AZIM_PI_WEDGE_CROSS_DOT
AZIM_PI_WEDGE_GE_CROSS_DOT
AZIM_PI_WEDGE_GE_SIN
AZIM_PI_WEDGE_SIN
AZIM_POS_IMP_CYCLIC_SET
AZIM_POS_IMP_SUM_2PI
AZIM_POS_IMP_SUM_2PI_ALT
AZIM_RANGE
AZIM_SAME_WITHIN_AFF_GE
AZIM_SAME_WITHIN_AFF_GE_ALT
AZIM_SPEC_DEGENERATE
AZIM_SPLIT_POINT
AZIM_SUM_LE
AZIM_ZERO_SHIFT
A_1
A_6I1_LE_A_6M1
A_6M1_EQ_6I1_EDGE
A_B_J_SCS_OPP
A_EQ2_IMP_B
A_EQ2h0_IMP_B
A_EQ_PSORT
A_LEMMA
A_LE_A_OVERRIDE
A_LT_B_4I1
A_LT_B_4I2
A_NOT_EQ2_IMP_B
A_POS_DELTA
a5_assumption_reduction
a_assumption_reduction
a_azim
a_bn_eq
a_ear0
a_node_fan
a_spine5
a_sy
a_tame
a_tau
a_ts
ab4_assumption_reduction
ab4_assumption_reduction2
ab4_assumption_reduction_sym
abc_of_quadratic
abc_param
abc_quadratic
abcd
abdodec
abs_1_prod
abs_lemma
abs_pass_through
acs3_hi
acs3_lo
acs_atn2
acs_partial_lemma'
acs_second_lemma'
acs_sqrt_x1_d4
acs_sqrt_x2_d4
acts
add6
add_diag
add_diag_list
add_edge_graph
add_edge_graph_fan
add_edge_imp_card_set_edge_ge1_fan
add_edge_into_collinear_fan
add_mod
add_partial_lemma'
add_second_lemma'
add_steps
add_steps_in_atom
addition_exponents
addition_sigma_fan
adjacent_pai
adjoint
adm_1
adm_2
adm_3
admissible_weight
adodec
aff
aff_2
aff_3_rep_cross_dot
aff_SUBSET
aff_affine
aff_comb
aff_eq_affcomb
aff_ge1_1_subset_aff_ge
aff_ge1_subset_aff_ge
aff_ge_0_2
aff_ge_0_2_SUBSET
aff_ge_0_2_eq_segment
aff_ge_1_1_subset_aff_fan
aff_ge_1_1_subset_aff_ge_fan
aff_ge_1_1_subset_xfan
aff_ge_1_3_eq_unions_aff_ge_1_2_and_aff_gt_1_3
aff_ge_2_1_is_exists_point_inaff_ge_1_2
aff_ge_3_1_rep_cross_dot
aff_ge_INTER_aff_lt
aff_ge_alt
aff_ge_def
aff_ge_eq_aff_gt_union_aff_ge
aff_ge_eq_lemma
aff_ge_inter_aff_ge
aff_ge_inter_segments
aff_ge_subset3_aff_ge
aff_ge_subset_aff_gt_union_aff
aff_ge_subset_aff_gt_union_aff_ge
aff_ge_trans
aff_gt12_subset_aff_ge
aff_gt1_subset_aff_ge
aff_gt1_subset_aff_gt
aff_gt2_subset_aff_ge
aff_gt3_subset_aff_gt
aff_gt_1_2_cross_dotr_4point
aff_gt_1_2_cross_dotr_4point_neg
aff_gt_1_2_cross_dotr_4point_zero
aff_gt_1_2_scale_fan
aff_gt_1_2_subset_aff_1_3111
aff_gt_1_3_eq_unions_aff_gt_1_2
aff_gt_1_3_subset_dart_leads_into_fan
aff_gt_1_3_subset_yfan
aff_gt_2_1_cross_dotl_4point
aff_gt_2_1_cross_dotr_4point
aff_gt_2_1_crossr_dot_4point
aff_gt_2_1_rcross_dot_4pointl
aff_gt_2_1r_rcross_dotl_4point
aff_gt_3_1_INTER_aff_SUBSET_aff_gt_2_1
aff_gt_3_1_INTER_aff_SUBSET_aff_gt_2_14
aff_gt_3_1_rep_cross_dot
aff_gt_add_subset_U1
aff_gt_connect_bound_not_inter_edges_fan
aff_gt_connect_bound_subset_yfan
aff_gt_def
aff_gt_eq_fanadd
aff_gt_imp_not_collinear
aff_gt_in_rw_dart_fan
aff_gt_in_w_dart_fan
aff_gt_inter_aff_gt
aff_gt_radial
aff_gt_subset_aff_ge
aff_gt_subset_component_y_fan
aff_gt_subset_dartset_leads_into_fan_union_aff_gt
aff_gt_subset_wedge_fan2
aff_imp_affcomb
aff_le_def
aff_lt_def
aff_normball
aff_subset_aff_ge
affcomb_imp_aff
affine
affine_INTERS
affine_aff
affine_affcomb
affine_comb
affine_dependent
affine_facet_hyper
affine_hull_2_fan
affine_hull_3_plane
affine_hull_e
affine_invert
affine_two_points
affpropos_lt_2_1
affprops
affprops_0_3
affprops_2_1
affprops_3_0
affprops_ge_2_1
affsign
all
all_n
all_voronoi_subset_ball
allpairs
alt_azim_fan_sum
anchor
anchor_alt
anchor_points
angle_is_small_fan
angle_is_smallpi_fan
angle_sum_5T1
ans
apex_A
apex_flat
apex_flat_h
apex_flat_hll
apex_flat_l
apex_std3_hll
apex_std3_lhh
apex_std3_lll_wxx
apex_std3_lll_xww
apex_std3_small_hll
apex_sup_flat
arc1553_v39
arcV
arcVarc
arc_1
arc_concave
arc_derivative
arc_derivative2
arc_hhn
arc_hhn'
arc_lemma1
arc_lemma3
arc_lemma4
arc_lemma5
arc_length1_increasing
arc_length2_increasing
arc_sym
archive3a
arclength
arclength'
arclength2
arclength222h0
arclength_2h0_cstab
arclength_lt_1553
arclength_pos_eq
arclength_x1
arclength_x1'
arclength_x2
arclength_x_123
arclength_x_123'
arclength_x_126
arclength_x_234
arclength_x_345
arclength_xrr
arclength_y1
arclength_y1'
arclength_y2
arcmax_v39
arg_diff
asn797k
asnFnhk
asn_sin_t''_alt
associative
at_fan
at_infinity_fan
atn2
atn2'
atn2_0y
atn2_atn_open
atn2_atn_open_2
atn2_atn_open_3
atn2_deriv_simple1
atn2_deriv_simple2
atn2_deriv_simple3
atn2_derivative
atn2_final_1
atn2_final_2
atn2_final_3
atn2_lemma
atn2_spec
atn2curry
atn_abs
atn_add
atn_add2
atn_bounds
atn_bounds_anti
atn_co_table
atn_half
atn_half_range
atn_halfatn4
atn_inv
atn_lemma
atn_lemma_2
atn_lemma_3
atn_notnegpi_lemma
atn_notpi_lemma
atn_partial_lemma'
atn_second_lemma'
atom
atom_eq
atom_one_point
atom_reflect
atom_sym
atom_trans
atom_via_choice
atomic_particles
attach
augmented_constraint_system1
augmented_constraint_system2
aux_ineq
aux_lemma1
aux_lemma2
aux_permutes_conversion
aux_th
avo
avoids1_fan
avoids_fan
azim1
azim2_fan
azim3_fan
azim5_reduction
azim_0_as_closed
azim_assumption_reduction
azim_axis
azim_continuous_when_not_coplanar
azim_cross_0
azim_cycle
azim_cycle_def
azim_cycle_distinct
azim_cycle_fan
azim_cycle_fan2
azim_cycle_hyp_def
azim_cycle_neg
azim_cycle_scale
azim_cycle_spec
azim_dart
azim_dart_azim_in_fan
azim_dart_nin_d1
azim_def
azim_dih_y
azim_dominated_split
azim_fan
azim_fanadd_eq
azim_fanadd_eq_ds
azim_ge_azim_dart
azim_hyp_def
azim_i_fan
azim_in_fan
azim_in_fan2
azim_in_fan_azim
azim_is_zero_fan
azim_line_fan
azim_list
azim_lt_pi_cross
azim_mcell
azim_mod
azim_pos
azim_pos_iff_nz
azim_pos_open
azim_real_continuous_on
azim_spec
azim_trangle_le_azim_face_fan
azimdart