HOL html

Files Index

Theorems Index

B (theorems)

B0_0
B0_ADD
B0_EXPLICIT
B0_SUC
BAISC_PROP_EQU
BALL_ANNULUS_3PONITS_ANGLE
BALL_ANNULUS_3PONITS_NORM_MIN
BALL_ANNULUS_4PONITS_AFF_GT
BALL_ANNULUS_SYM_0
BALL_CONVEX_HULL_LEMMA
BALL_DIFF_RCONE_GT
BALL_DIFF_RCONE_GT_BISECTOR
BALL_EQ_EMPTY_FAN
BALL_LINEAR_INVARIANT
BALL_SUBSET_BIS_LE
BALL_SUBSET_BIS_LT
BALL_SUBSET_CBALL_FAN
BARV
BARV3_SET_OF_LIST4
BARV3_TRUNC1
BARV3_TRUNC2
BARV_0
BARV_2_EXPLICIT
BARV_2_IMP_NOT_COLLINEAR_SET_OF_LIST
BARV_3_EXPLICIT
BARV_3_IMP_FINITE_lemma1
BARV_3_IMP_FINITE_lemma2
BARV_AFFINE_INDEPENDENT
BARV_CARD_LEMMA
BARV_CIRCUMCENTER_EXISTS
BARV_CIRCUMCENTER_PROJECTION
BARV_CONS
BARV_DISTINCT
BARV_EXISTS
BARV_EXISTS_ALT
BARV_IMP_HD_IN_SET_OF_LIST
BARV_IMP_HL_1_POS_LT
BARV_IMP_K_LE_3
BARV_IMP_LENGTH_EQ_CARD
BARV_IMP_VORONOI_LIST_NOT_EMPTY
BARV_IMP_u0_IN_V
BARV_INITIAL_SUBLIST
BARV_K_EXPLICIT
BARV_LENGTH_LEMMA
BARV_SUBSET
BAR_TRI
BAR_WI_LONG_ED
BASED_POINT2
BASE_IN_VORONOI_CLOSED
BASE_POINT_FAN_LINEAR_IMAGE_EQ
BASE_POINT_FAN_TRANSLATION_EQ
BASIC_HALF_SLICE
BASIC_HALF_SLICE_STAB
BASIC_IMP_NOT_J
BASIC_MM_EQ_BBPRIME2
BASIC_MM_EQ_BBPRIME2_POINT
BASIC_OPP
BASIS_3
BASIS_CARD_EQ_DIM
BASIS_COMPONENT
BASIS_EQ_0
BASIS_EXISTS
BASIS_EXISTS_FINITE
BASIS_EXPANSION
BASIS_EXPANSION_UNIQUE
BASIS_HAS_SIZE_DIM
BASIS_HAS_SIZE_UNIV
BASIS_INJ
BASIS_NE
BASIS_NONZERO
BASIS_ORTHOGONAL
BASIS_SUBSPACE_EXISTS
BBINDEX_BBPRIME_LE_SUBDIVISION1
BBINDEX_BBPRIME_LE_SUBDIVISION2
BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
BBINDEX_EQ_SUBDIVISION
BBINDEX_EQ_SUBDIVISION1
BBINDEX_EQ_SUBDIVISION_C_EQ_AM
BBINDEX_EQ_SYM_0
BBINDEX_MIN_SYM_0
BBINDEX_MIN_S_LE_SUBDIVISION1
BBINDEX_MIN_S_LE_SUBDIVISION2
BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM
BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
BBPRIME2_SYM_0
BBPRIME_EQ_OPP_SYM_0
BBPRIME_IMP_BB
BBPRIME_SUBDIVISION2_SUBSET_BBPRIME
BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1
BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM
BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
BBPRIME_SUBSET_SUBDIVISION_UNION
BBS_IMP_CONVEX_LOCAL_FAN
BB_3M1_prime_IMP_scs_3M1
BB_3T1_prime_IMP_scs_3T1
BB_3T3_prime_IMP_scs_3T3
BB_3T4_prime2_IMP_scs_3T4
BB_3T4_prime_IMP_scs_3T4
BB_4I3_IMP_4T4
BB_4I3_IMP_BB_4M6
BB_4I3_IMP_BB_STAN_4I3
BB_4M2_IMP_BB_4M6
BB_4M2_IMP_BB_STAN_4M2
BB_4M3_IMP_BB_4M6
BB_4M3_IMP_BB_STAN_4M3
BB_4M4_IMP_BB_4M7
BB_4M4_IMP_BB_STAN_4M4
BB_4M5_IMP_BB_4M8
BB_4M5_IMP_BB_STAN_4M5
BB_4M6_IMP_4T5
BB_4M6_IMP_BB_STAN_4M6
BB_4M6_IMP_scs_4T3
BB_4M6_prime_IMP_scs_4M6
BB_4M7_IMP_4M6_01
BB_4M7_IMP_4M6_12
BB_4M7_IMP_BB_STAN_4M7
BB_4M7_prime_IMP_scs_4M7
BB_4M8_IMP_4M6_01
BB_4M8_IMP_4M6_23
BB_4M8_IMP_BB_STAN_4M8
BB_4M8_IMP_scs_4M8_02
BB_4M8_IMP_scs_4M8_13
BB_4M8_prime_IMP_scs_4M8
BB_5I1_IS_BB_5M2
BB_5I2_IS_BB_5M2
BB_5I3_IS_BB_5M1
BB_5I3_IS_BB_5M2
BB_5M1_IS_BB_5M2
BB_6I1_IS_BB_6M1
BB_EQ_UNION_BB_SUBDIVISION
BB_F_SUC_PRE
BB_INTER_BBPRIME_SUBDIVISION2
BB_RHO_NODE_IVS
BB_TRANS_SUBSET_BB
BB_VV_FUN_EQ
BBindex_min_LE_SUBDIVISION1
BBindex_min_LE_SUBDIVISION2
BBindex_min_LE_SUBDIVISION2_C_EQ_AM
BBindex_min_v39
BBindex_v39
BBprime2_v39
BBprime_v39
BBs_inj
BBs_v39
BC_DEL_FOR
BDXKHTW
BDXKHTW_PREP_LEMMA
BEGIN_POINT_PERIODIC
BETA_BUMP_ALT
BETA_BUMP_INVOLUTION
BETA_BUMP_INVOLUTION_BIJ
BETA_BUMP_INVOLUTION_CRITICAL
BETA_BUMP_INVOLUTION_NEG
BETA_BUMP_NZ
BETA_ORDERED_PAIR_THM
BETA_PAIR_THM
BETA_SET_2_THM
BETWEEN_ANTISYM
BETWEEN_DOT
BETWEEN_IFF_IN_CONVEX_HULL
BETWEEN_IMP_COLLINEAR
BETWEEN_IMP_IN_CONVEX_HULL
BETWEEN_MIDPOINT
BETWEEN_NORM
BETWEEN_PROJ_POINT
BETWEEN_REFL
BETWEEN_REFL_EQ
BETWEEN_SYM
BETWEEN_TRANS
BETWEEN_TRANS_2
BETWEEN_TRANS_3_CASES
BGMIFTE
BIEFJHU_explicit
BIJ_ALT
BIJ_AND_BIJ_INVERSE
BIJ_AND_MAP_COMM
BIJ_AZIM_CYCLE_EE
BIJ_BETWEEN_FF_AND_V
BIJ_CARD
BIJ_CARD_EQ
BIJ_DART_POLYEDGE
BIJ_EDGES_DART_FACE
BIJ_EXTENDS_INJ
BIJ_FACET2_EDGE
BIJ_FACET_HYPERFACE
BIJ_FINITE_TOO
BIJ_IMP_CARD_EQ
BIJ_IMP_RES_INVERSE
BIJ_INVERSE
BIJ_NUMSEG
BIJ_RES_INVERSE
BIJ_SUM
BIJ_SYM
BIJ_TRANS
BILINEAR_BOUNDED
BILINEAR_BOUNDED_POS
BILINEAR_EQ
BILINEAR_EQ_STDBASIS
BILINEAR_LADD
BILINEAR_LMUL
BILINEAR_LNEG
BILINEAR_LSUB
BILINEAR_LZERO
BILINEAR_RADD
BILINEAR_RMUL
BILINEAR_RNEG
BILINEAR_RSUB
BILINEAR_RZERO
BILINEAR_VSUM
BILINEAR_VSUM_PARTIAL_PRE
BILINEAR_VSUM_PARTIAL_SUC
BIS_EQ_HYPERPLANE
BIS_FACE_OF_BIS_LE
BIS_HYPERPLANE
BIS_LE
BIS_LE_EQ_HALFSPACE
BIS_LE_INTER
BIS_LE_NORM
BIS_LE_UNION
BIS_LT
BIS_LT_NORM
BIS_SYM
BKOSSGE
BNAWVNH
BODE_YEU_ANH_DI
BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN
BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN
BOOL_MODEL_PERIODIC_SMALL
BOUNDARY_VOLUME
BOUNDED_BALL_ANNULUS
BOUNDED_BALL_FAN
BOUNDED_CBALL_FAN
BOUNDED_CLOSED_IMP_COMPACT_FAN
BOUNDED_CLOSED_NEST_FAN
BOUNDED_CLOSURE_FAN
BOUNDED_EMPTY_FAN
BOUNDED_FUNCTIONS_BIJECTIONS_1
BOUNDED_FUNCTIONS_BIJECTIONS_2
BOUNDED_HAS_INF_FAN
BOUNDED_HAS_SUP_FAN
BOUNDED_HYPERPLANE_EQ_TRIVIAL
BOUNDED_INTER_BALL
BOUNDED_INTER_FAN
BOUNDED_LIFT_FAN
BOUNDED_MATVEC
BOUNDED_MCELL
BOUNDED_PASTECART_FAN
BOUNDED_POS_FAN
BOUNDED_SING
BOUNDED_SUBSET_FAN
BOUNDED_SY
BOUNDED_TRI_SY
BOUNDED_UNION_FAN
BOUNDED_VOLUME_MCELL
BOUNDED_VORONOI_CLOSED
BOUNDED_VORONOI_LIST
BOUNDS_V4_klemma
BOUNDS_VGEN_klemma
BOUND_BETA_BUMP
BOUND_GAMMA_X_lmfun
BPOW8APOW2CPOW2
BSXAQBQ
BUTLAST_APPEND_SING
BUTLAST_INITIAL_SUBLIST
BZQNDMN
B_6I1_LE_B_6M1
B_EQ_PSORT
B_LE_2h0_2_SCS_M_4
B_LE_2h0_2_SCS_M_4_1
B_LE_2h0_A_EQ2_IN_CASES_6
B_LE_2h0_IMP_B
B_LE_2h0_SCS_M_4
B_LE_CSTAB_5I1
B_LE_CSTAB_5M2
B_LE_CSTAB_5M2_A_LT_B
B_LE_CSTAB_6M1
B_LE_CSTAB_SCS_4I1
B_LE_CSTAB_SCS_4I2
B_LE_CSTAB_SCS_4I2_prime
B_LE_CSTAB_SCS_4I3
B_OVERRIDE_LE_B
B_SY1
B_SY_LE_CSTAB
b0_thm
b1
b5_assumption_reduction
b_assumption_reduction
b_bn_eq
b_ear0
b_spine5
b_sy
b_tame
b_ts
back
back_and_loop_darts
back_tail_outside_atom
ball3_lambda
ball_annulus
ball_eq_normball
ball_fan
ball_subset_union_ccube
ballnorm_fan
ballsets_fan
barrier
barrier'
base_point_fan
basic_examples
basis
bcc_value
bdd_num_func_attain_max
bdodec
bdt1_finiteness
bdt2_finiteness
bdt3_finiteness
bdt4_finiteness
bdt5_finiteness
bdt6_finiteness
bdt7_finiteness
bdt_canbatrenbon
bdt_emnguchua
bdt_emveque
behead
belast
belong
beta_bumpA
beta_bumpA_lb0
beta_bumpA_lb1
beta_bumpA_y
beta_bumpA_y_NONBETA
beta_bumpA_y_lb
beta_bumpA_y_sym23
beta_bump_force_x
beta_bump_force_y
beta_bump_lb
beta_bump_v1
beta_lb
beta_sub
beta_ub
between
between'
bij_cube
bijective
bilinear
bis
bis_le
bis_lt
bisector_point
bisector_point_exists
bn_Faces
bn_PlaneGraphs
bn_PlaneGraphsP
bn_RTranCl
bn_Seed
bn_admissible
bn_admissible1
bn_admissible2
bn_admissible3
bn_cong_iso
bn_cong_iso_refl
bn_cong_pr_iso
bn_congs
bn_containsDuplicateEdge
bn_containsDuplicateEdge0
bn_containsUnacceptableEdge
bn_containsUnacceptableEdgeSnd
bn_countNonFinals
bn_countVertices
bn_degree
bn_directedLength
bn_duplicateEdge
bn_edges
bn_edges_graph
bn_enumAppend
bn_enumBase
bn_enumTab
bn_enumerator
bn_enumt
bn_except
bn_exceptionalVertex
bn_excessTCount
bn_faceListAt
bn_faces
bn_facesAt
bn_fgraph
bn_finalGraph
bn_finalVertex
bn_final_face
bn_finals
bn_generatePolygon
bn_graph
bn_height
bn_heights
bn_heightsNewVertices
bn_hideDups
bn_hideDupsRec
bn_indexToVertexList
bn_inj_on
bn_invariant
bn_isTable
bn_is_Hom
bn_is_Iso
bn_is_hom
bn_is_iso
bn_is_pr_Iso
bn_is_pr_iso
bn_iso_in
bn_iso_subseteq
bn_makeFaceFinal
bn_makeFaceFinalFaceList
bn_mapAt
bn_maxGon
bn_minimal
bn_minimalFace
bn_minimalVertex
bn_neighbors
bn_nextElem
bn_nextVertex
bn_nextVertices
bn_next_plane
bn_noExceptionals
bn_nonFinals
bn_pr_iso_in
bn_pr_iso_subseteq
bn_prevVertex
bn_quad
bn_removeKey
bn_removeKeyList
bn_replacefacesAt
bn_setFinal
bn_splitFace
bn_split_face
bn_squanderFace
bn_squanderTarget
bn_squanderVertex
bn_sub
bn_sub1
bn_subdivFace
bn_subdivFace0
bn_tabulate
bn_tabulate0
bn_tabulate2
bn_tabulate3
bn_tame
bn_tame10
bn_tame11a
bn_tame11b
bn_tame12o
bn_tame13a
bn_tame9a
bn_tri
bn_triangle
bn_vertextype
bn_vertices_face
bn_vertices_graph
bn_vertices_set
border
bound_for_pi
bound_square
bound_voronoi
bounded_ballnorm_fan
bounded_ballnorm_fans
bounded_convex1_fan
bounded_convex_fan
bounded_fan
bounded_on
bounded_on_int
bp_bdt
bth
bump