HOL html

Files Index

Theorems Index

V (theorems)

V
V3_DEFOR_CONVEX_LOCAL_FAN_MK
V3_DEFOR_CONVEX_LOCAL_FAN_MK_TWO_CASES
V3_DEFOR_DEFORMATION
V3_DEFOR_DEFORMATION_CONVEX_LOCAL_FAN
V3_DEFOR_DEFORMATION_CONVEX_LOCAL_FAN_V1
V3_DEFOR_DEFORMATION_CONVEX_LOCAL_FAN_V1_TWO_CASES
V3_DEFOR_DEFORMATION_V5
V3_DEFOR_EQ_IN_FF
V3_DEFOR_EQ_IN_FF_AT_V1
V3_DEFOR_EQ_IN_FF_AT_V1_SYM
V3_DEFOR_EQ_IN_FF_AT_V1_SYM_V1
V3_DEFOR_EQ_IN_FF_AT_V1_SYM_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_AT_V1_V1
V3_DEFOR_EQ_IN_FF_AT_V1_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_AT_V_ANY
V3_DEFOR_EQ_IN_FF_AT_V_ANY_SYM
V3_DEFOR_EQ_IN_FF_AT_V_ANY_SYM_V1
V3_DEFOR_EQ_IN_FF_AT_V_ANY_SYM_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_AT_V_ANY_V1
V3_DEFOR_EQ_IN_FF_AT_V_ANY_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_AT_W
V3_DEFOR_EQ_IN_FF_AT_W_SYM
V3_DEFOR_EQ_IN_FF_AT_W_SYM_V1
V3_DEFOR_EQ_IN_FF_AT_W_SYM_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_AT_W_V1
V3_DEFOR_EQ_IN_FF_AT_W_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_MK
V3_DEFOR_EQ_IN_FF_MK_SYM
V3_DEFOR_EQ_IN_FF_MK_SYM_TWO_CASES
V3_DEFOR_EQ_IN_FF_MK_TWO_CASES
V3_DEFOR_EQ_IN_FF_NOT_MK
V3_DEFOR_EQ_IN_FF_NOT_MK_SYM
V3_DEFOR_EQ_IN_FF_NOT_MK_SYM_TWO_CASES
V3_DEFOR_EQ_IN_FF_NOT_MK_TWO_CASES
V3_DEFOR_EQ_IN_FF_SUB_MK
V3_DEFOR_EQ_IN_FF_SUB_MK_SYM
V3_DEFOR_EQ_IN_FF_SUB_MK_SYM_TWO_CASES
V3_DEFOR_EQ_IN_FF_SUB_MK_TWO_CASES
V3_DEFOR_EQ_IN_FF_SUC_MK
V3_DEFOR_EQ_IN_FF_SUC_MK_SYM
V3_DEFOR_EQ_IN_FF_SUC_MK_SYM_TWO_CASES
V3_DEFOR_EQ_IN_FF_SUC_MK_TWO_CASES
V3_DEFOR_EQ_IN_FF_SYM
V3_DEFOR_EQ_IN_FF_SYM_V1
V3_DEFOR_EQ_IN_FF_SYM_V1_TWO_CASES
V3_DEFOR_EQ_IN_FF_V1
V3_DEFOR_EQ_IN_FF_V1_TWO_CASES
V3_DEFOR_ID
V3_DEFOR_INCREASING_IN_ANGLE
V3_DEFOR_IN_AFF_GT
V3_DEFOR_IN_AFF_GT_V1
V3_DEFOR_IN_AFF_GT_V1_MK
V3_DEFOR_IN_BALL_ANNULUS_DEFORMATION
V3_DEFOR_RHO_NODE
V3_DEFOR_RHO_NODE_AT_V1
V3_DEFOR_RHO_NODE_AT_V1_V1
V3_DEFOR_RHO_NODE_AT_V1_V1_TWO_CASES
V3_DEFOR_RHO_NODE_V1
V3_DEFOR_RHO_NODE_V1_TWO_CASES
V3_DEFOR_V1_EQV3_DEFOR_V2
V3_DEFOR_V1_O_DEF
V5_IN_AFF21_IMP_SET_EQ
VAR_ADD_THM
VAR_MUL_THM
VASYYAU
VBTIKLP
VBVYGGT
VC
VC1
VCRJIHC
VC_DISJOINT
VC_INFI
VC_INFI_trg
VC_trg
VCt
VEC0_BALL_ANNULUS
VEC0_BOTH_LT_GT
VEC0_NOT_COLLINEAR_SYM_0
VEC0_SYM_0
VEC0_UNION_SYM_0
VEC2_PRE_TRIG_FORM
VEC3_EQ_EX
VECMATS_MATVEC_ID
VECMAT_ADD
VECMAT_CMUL
VECMAT_NEG
VECMAT_ROW
VECMAT_SUB
VECMAT_VEC
VECTOR_1
VECTOR_2
VECTOR_3
VECTOR_3_3
VECTOR_3_4
VECTOR_3_5
VECTOR_3_6
VECTOR_ADD_AC
VECTOR_ADD_ASSOC
VECTOR_ADD_COMPONENT
VECTOR_ADD_COMPONENT_3
VECTOR_ADD_LDISTRIB
VECTOR_ADD_LID
VECTOR_ADD_LINV
VECTOR_ADD_RDISTRIB
VECTOR_ADD_RID
VECTOR_ADD_RINV
VECTOR_ADD_SUB
VECTOR_ADD_SYM
VECTOR_ANGLE_DOUBLECROSS
VECTOR_CHOOSE_DIST
VECTOR_CHOOSE_SIZE
VECTOR_COMPONENT
VECTOR_COMPONENTS_3
VECTOR_COMPONENTWISE
VECTOR_EQ
VECTOR_EQ_ADDR
VECTOR_EQ_COMPONENT
VECTOR_EQ_LDOT
VECTOR_EQ_RDOT
VECTOR_IN_ORTHOGONAL_BASIS
VECTOR_IN_ORTHOGONAL_SPANNINGSET
VECTOR_IN_ORTHONORMAL_BASIS
VECTOR_LAW_OF_SINES
VECTOR_MATRIX_MUL_TRANSP
VECTOR_MUL_ASSOC
VECTOR_MUL_COMPONENT
VECTOR_MUL_COMPONENT_3
VECTOR_MUL_EQ_0
VECTOR_MUL_LCANCEL
VECTOR_MUL_LCANCEL_IMP
VECTOR_MUL_LID
VECTOR_MUL_LNEG
VECTOR_MUL_LZERO
VECTOR_MUL_RCANCEL
VECTOR_MUL_RCANCEL_IMP
VECTOR_MUL_RNEG
VECTOR_MUL_RZERO
VECTOR_NEG_0
VECTOR_NEG_COMPONENT
VECTOR_NEG_COMPONENT_3
VECTOR_NEG_EQ_0
VECTOR_NEG_MINUS1
VECTOR_NEG_NEG
VECTOR_NEG_SUB
VECTOR_OF_DIHV_ORTHONORMAL
VECTOR_ONE
VECTOR_PROJECTION
VECTOR_SCALE_CHANGE
VECTOR_SUB
VECTOR_SUB_ADD
VECTOR_SUB_ADD2
VECTOR_SUB_COMPONENT
VECTOR_SUB_COMPONENT_3
VECTOR_SUB_DISTRIBUTE
VECTOR_SUB_EQ
VECTOR_SUB_LDISTRIB
VECTOR_SUB_LZERO
VECTOR_SUB_PROJECT_ORTHOGONAL
VECTOR_SUB_RADD
VECTOR_SUB_RDISTRIB
VECTOR_SUB_REFL
VECTOR_SUB_RZERO
VEC_COMPONENT
VEC_COMPONENT_3
VEC_DIV_MOV
VEC_EQ
VEC_PER2_3
VIET_THEOREM
VMUL_CASES
VOLUME_CONIC_CAP_WEDGE_GE_VS_CONIC_CAP
VOLUME_FIX
VOLUME_PROPS_CONIC_CAP
VOLUME_PROPS_CONV0
VOLUME_PROPS_FRUSTT
VOLUME_PROPS_IMAGE
VOLUME_PROPS_MEASURABLE
VOLUME_PROPS_NORMBALL
VOLUME_PROPS_NULLSET
VOLUME_PROPS_RECT
VOLUME_PROPS_SCALE
VOLUME_PROPS_SDIFF
VOLUME_PROPS_SOLID_TRIANGLE
VOL_DISJOINT_UNION
VOL_NULLSET_UNION
VOL_POS_LT_AFF_DIM_3
VOL_UNION_LE
VORO2_EX
VORONOI_BALL2
VORONOI_BARV_CANONICAL
VORONOI_CLOSED
VORONOI_CLOSED_ALT
VORONOI_CLOSED_AS_FINITE_INTERSECTION
VORONOI_CLOSED_AS_INTERSECTION
VORONOI_CLOSED_CONTAINS_BALL
VORONOI_CLOSED_EQ_FINITE_INTERS_BIS_LE
VORONOI_CLOSED_EQ_INTERS_BIS_LE
VORONOI_CLOSED_EQ_INTERS_BIS_LE_ALT
VORONOI_CLOSED_EQ_LEMMA
VORONOI_CLOSED_PARTITION
VORONOI_CLOSED_PARTITION_STRONG
VORONOI_CLOSED_SUBSET_BALL
VORONOI_CONV
VORONOI_INTER_BIS_EQ_INTER_BIS_LE
VORONOI_INTER_BIS_LE
VORONOI_LIST
VORONOI_LIST_3_SINGLETON_EXPLICIT
VORONOI_LIST_AFF_DIM
VORONOI_LIST_ALMOST_CANONICAL
VORONOI_LIST_ALMOST_CANONICAL_0
VORONOI_LIST_BIS
VORONOI_LIST_BIS_LE
VORONOI_LIST_CANONICAL
VORONOI_LIST_EQ
VORONOI_LIST_EQ_INTERS_BIS
VORONOI_LIST_EQ_UNION_CONVEX_HULL_FACETS
VORONOI_LIST_INTER_BIS
VORONOI_LIST_SING
VORONOI_LIST_SUBSET_VORONOI_CLOSED
VORONOI_NONDG
VORONOI_OPEN
VORONOI_OPEN_AS_FINITE_INTERSECTION
VORONOI_OPEN_AS_INTERSECTION
VORONOI_OPEN_SUBSET_CLOSED
VORONOI_POLYHEDRON
VORONOI_SET
VORONOI_SET_2
VORONOI_SET_2_BIS
VORONOI_SET_2_BIS_LE
VORONOI_SET_SING
VORONOI_SET_SUBSET
VORONOI_V
VPWSHTO
VPWSHTO1
VPWSHTO2
VPWSHTO200
VPWSHTO_PRIME
VQFYMZY
VSMPQYO
VSUM
VSUM_0
VSUM_1
VSUM_2
VSUM_3
VSUM_ADD
VSUM_ADD_GEN
VSUM_ADD_NUMSEG
VSUM_ADD_SPLIT
VSUM_BIJECTION
VSUM_CASES
VSUM_CASES_1
VSUM_CLAUSES
VSUM_CLAUSES_LEFT
VSUM_CLAUSES_NUMSEG
VSUM_CLAUSES_RIGHT
VSUM_CLAUSES_alt
VSUM_CMUL_NUMSEG
VSUM_COMBINE_L
VSUM_COMBINE_R
VSUM_COMPONENT
VSUM_CONST
VSUM_CONST_NUMSEG
VSUM_DELETE
VSUM_DELETE_CASES
VSUM_DELTA
VSUM_DIFF
VSUM_DIFFS
VSUM_DIFFS_ALT
VSUM_DIS2
VSUM_DIS3
VSUM_DIS4
VSUM_EQ
VSUM_EQ_0
VSUM_EQ_GENERAL
VSUM_EQ_GENERAL_INVERSES
VSUM_EQ_NUMSEG
VSUM_EQ_SUPERSET
VSUM_GROUP
VSUM_IMAGE
VSUM_IMAGE_GEN
VSUM_IMAGE_NONZERO
VSUM_INCL_EXCL
VSUM_INJECTION
VSUM_LMUL
VSUM_NEG
VSUM_NORM
VSUM_NORM_ALLSUBSETS_BOUND
VSUM_NORM_BOUND
VSUM_NORM_LE
VSUM_NORM_TRIANGLE
VSUM_OFFSET
VSUM_OFFSET_0
VSUM_PAIR
VSUM_PAIR_0
VSUM_PARTIAL_PRE
VSUM_PARTIAL_SUC
VSUM_REAL
VSUM_RESTRICT
VSUM_RESTRICT_SET
VSUM_RMUL
VSUM_SING
VSUM_SING_NUMSEG
VSUM_SUB
VSUM_SUB_NUMSEG
VSUM_SUC
VSUM_SUPERSET
VSUM_SWAP
VSUM_SWAP_NUMSEG
VSUM_TRIV_NUMSEG
VSUM_UNION
VSUM_UNIONS_NONZERO
VSUM_UNION_LZERO
VSUM_UNION_NONZERO
VSUM_UNION_RZERO
VSUM_VMUL
VSUM_VSUM_PRODUCT
VV_INJ
VV_SUC_EQ_IVS_RHO_NODE_PRIME
VV_SUC_EQ_RHO_NODE
VV_SUC_EQ_RHO_NODE_PRIME
VX
VX_EMPTY
V_AZIM_SMALLEST_ELMS
V_CELL0_EMPTY
V_CELL1_SINGLE
V_DEFORMATION_V3_DEFOR
V_DEFORMATION_V3_DEFOR_V5
V_DEFORMATION_WW_DEFOR
V_E_FF_CASE_4
V_E_FF_CASE_4_3
V_E_FF_CASE_4_sqrt8
V_E_FF_CASE_5
V_E_FF_CASE_5_pro_cs
V_E_FF_CASE_5_sqrt8
V_E_FF_CASE_6
V_E_FF_IS_SCS_CASES_3
V_E_FF_IS_SCS_CASES_4
V_E_FF_IS_SCS_CASES_5
V_E_FF_IS_SCS_CASES_6
V_IN_DARTS_IFF_E_V_IN_DARTS
V_IN_DARTS_IMP_SWICH_SO_DO
V_PRIME_EQ_V_vv
V_PRIME_SUBSET_V
V_SLICE_EQ_NUMSEG
V_SY
v1_in_convex3
v1v2v3_in_convex3
v3_defor_v1
v3_defor_v2
v3_defor_v4
v3_defor_v5
v3_in_convex3
v_hat
v_prime
v_std
v_subset_xfan
value_next_of_head
varith
vcross_e3_fan
vdot_e1_fan
vdot_e2_fan
vec
vec_le
vecmat
vecmats
vector6
vector6_comp
vector_add
vector_eq1
vector_eq2
vector_matrix_mul
vector_mul
vector_neg
vector_norm
vector_of_list
vector_of_simplex_dot
vector_of_simplex_edge_lemma
vector_sub
vector_to_pair
version_JUTSTKG
vertex_datum
vertex_slice
vol2f
vol2f_marchal_pow_y
vol2r
vol2r_y
vol3_vol_x
vol3_x_135_s2
vol3_x_sqrt
vol3f
vol3f_135_palt
vol3f_456
vol3f_lm0
vol3f_lmln
vol3f_palt
vol3f_sqrt2_lmplus
vol3f_x_lfun
vol3f_x_lfun_alt
vol3f_x_sqrt2_lmplus
vol3f_x_sqrt2_lmplus_alt
vol3fu_large
vol3r
vol3r_126_x
vol3r_alt
vol3rl
vol4f
vol4f_alt
vol4f_lmfun
vol4f_palt
volR
vol_ball_wedge
vol_conic_cap_wedge
vol_conv
vol_def
vol_frustt_wedge
vol_rect
vol_solid_triangle
vol_solid_triangle_ortho
vol_x
vol_x_y
vol_xl
vol_y
vol_y_e
vol_yl
volan
volume_ball_gon
volume_prop_fix
volume_props
voro2
voronoi
voronoi2
voronoi_closed
voronoi_in_ball
voronoi_le
voronoi_open
voronoi_subset_ball
voronoi_trg
voronoi_version2
vsum
vuy1
vuy2
vuy3
vuy4
vuy5
vv_azim_le
vv_azim_le_alt
vv_enclosed4
vv_inj_lemma
vv_quad_split012
vv_quad_split123
vv_quad_split_short
vv_rho_node1
vv_split_azim
vv_split_azim_alt
vv_split_azim_generic