HOL html

Files Index

Theorems Index

V (theorems)

VALID_PATH_CIRCLEPATH
VALID_PATH_COMPOSE
VALID_PATH_IMP_PATH
VALID_PATH_JOIN
VALID_PATH_JOIN_EQ
VALID_PATH_LINEPATH
VALID_PATH_PARTCIRCLEPATH
VALID_PATH_REVERSEPATH
VALID_PATH_SHIFTPATH
VALID_PATH_SUBPATH
VALID_PATH_VECTOR_POLYNOMIAL_FUNCTION
VARIATION_EQUAL_LEMMA
VECTOR_1
VECTOR_2
VECTOR_3
VECTOR_4
VECTOR_ADD_AC
VECTOR_ADD_ASSOC
VECTOR_ADD_COMPONENT
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_AFFINITY_EQ
VECTOR_ANGLE
VECTOR_ANGLE_1
VECTOR_ANGLE_ANGLE
VECTOR_ANGLE_ARG
VECTOR_ANGLE_COMPLEX_LMUL
VECTOR_ANGLE_EQ
VECTOR_ANGLE_EQ_0
VECTOR_ANGLE_EQ_0_DIST
VECTOR_ANGLE_EQ_0_LEFT
VECTOR_ANGLE_EQ_0_RIGHT
VECTOR_ANGLE_EQ_PI
VECTOR_ANGLE_EQ_PI_DIST
VECTOR_ANGLE_EQ_PI_LEFT
VECTOR_ANGLE_EQ_PI_RIGHT
VECTOR_ANGLE_LINEAR_IMAGE_EQ
VECTOR_ANGLE_LMUL
VECTOR_ANGLE_LNEG
VECTOR_ANGLE_NEG2
VECTOR_ANGLE_RANGE
VECTOR_ANGLE_REFL
VECTOR_ANGLE_RMUL
VECTOR_ANGLE_RNEG
VECTOR_ANGLE_SYM
VECTOR_CHOOSE_DIST
VECTOR_CHOOSE_SIZE
VECTOR_COMPONENTWISE
VECTOR_DERIVATIVE_AT
VECTOR_DERIVATIVE_CIRCLEPATH
VECTOR_DERIVATIVE_CONST_AT
VECTOR_DERIVATIVE_LINEPATH_AT
VECTOR_DERIVATIVE_LINEPATH_WITHIN
VECTOR_DERIVATIVE_PARTCIRCLEPATH
VECTOR_DERIVATIVE_UNIQUE_AT
VECTOR_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL
VECTOR_DERIVATIVE_WITHIN_CLOSED_INTERVAL
VECTOR_DERIVATIVE_WITHIN_INTERIOR
VECTOR_DERIVATIVE_WORKS
VECTOR_DIFF_CHAIN_AT
VECTOR_DIFF_CHAIN_WITHIN
VECTOR_EQ
VECTOR_EQ_ADDR
VECTOR_EQ_AFFINITY
VECTOR_EQ_DOT_SPAN
VECTOR_EQ_LDOT
VECTOR_EQ_NEG2
VECTOR_EQ_RDOT
VECTOR_EXPAND_1
VECTOR_EXPAND_2
VECTOR_EXPAND_3
VECTOR_EXPAND_4
VECTOR_IN_ORTHOGONAL_BASIS
VECTOR_IN_ORTHOGONAL_SPANNINGSET
VECTOR_IN_ORTHONORMAL_BASIS
VECTOR_MATRIX_MUL_TRANSP
VECTOR_MUL_ASSOC
VECTOR_MUL_COMPONENT
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_EQ_0
VECTOR_NEG_MINUS1
VECTOR_NEG_NEG
VECTOR_NEG_SUB
VECTOR_ONE
VECTOR_POLYNOMIAL_FUNCTION_ADD
VECTOR_POLYNOMIAL_FUNCTION_CMUL
VECTOR_POLYNOMIAL_FUNCTION_COMPONENT
VECTOR_POLYNOMIAL_FUNCTION_CONST
VECTOR_POLYNOMIAL_FUNCTION_ID
VECTOR_POLYNOMIAL_FUNCTION_MUL
VECTOR_POLYNOMIAL_FUNCTION_NEG
VECTOR_POLYNOMIAL_FUNCTION_SUB
VECTOR_POLYNOMIAL_FUNCTION_VSUM
VECTOR_SUB
VECTOR_SUB_ADD
VECTOR_SUB_ADD2
VECTOR_SUB_COMPONENT
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
VECTOR_VARIATION_COMBINE
VECTOR_VARIATION_CONST
VECTOR_VARIATION_CONST_EQ
VECTOR_VARIATION_CONTINUOUS
VECTOR_VARIATION_CONTINUOUS_LEFT
VECTOR_VARIATION_CONTINUOUS_RIGHT
VECTOR_VARIATION_EQ
VECTOR_VARIATION_GE_DROP_FUNCTION
VECTOR_VARIATION_GE_NORM_FUNCTION
VECTOR_VARIATION_INTEGRAL_NORM_DERIVATIVE
VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE
VECTOR_VARIATION_MONOTONE
VECTOR_VARIATION_NEG
VECTOR_VARIATION_ON_DIVISION
VECTOR_VARIATION_ON_NULL
VECTOR_VARIATION_POS_LE
VECTOR_VARIATION_REFLECT
VECTOR_VARIATION_REFLECT_INTERVAL
VECTOR_VARIATION_TRIANGLE
VEC_COMPONENT
VEC_EQ
VERTICES_LINEAR_IMAGE
VERTICES_TRANSLATION
VOLUME_BALL
VOLUME_BALL_WEDGE
VOLUME_CBALL
VOLUME_CONIC_CAP
VOLUME_CONIC_CAP_COMPL
VOLUME_CONIC_CAP_STRONG
VOLUME_CONIC_CAP_WEDGE
VOLUME_CONIC_CAP_WEDGE_MEDIUM
VOLUME_CONIC_CAP_WEDGE_WEAK
VOLUME_FRUSTT
VOLUME_FRUSTT_STRONG
VOLUME_FRUSTT_WEDGE
VOLUME_OF_CLOSED_TETRAHEDRON
VOLUME_OF_TETRAHEDRON
VOLUME_SOLID_TRIANGLE
VSUM
VSUM_0
VSUM_1
VSUM_2
VSUM_3
VSUM_4
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_CMUL_NUMSEG
VSUM_COMBINE_L
VSUM_COMBINE_R
VSUM_COMPLEX_LMUL
VSUM_COMPLEX_RMUL
VSUM_COMPONENT
VSUM_CONST
VSUM_CONST_NUMSEG
VSUM_CONTENT_NULL
VSUM_CX
VSUM_CX_NUMSEG
VSUM_DELETE
VSUM_DELETE_CASES
VSUM_DELTA
VSUM_DIFF
VSUM_DIFFS
VSUM_DIFFS_ALT
VSUM_DIFF_LEMMA
VSUM_EQ
VSUM_EQ_0
VSUM_EQ_GENERAL
VSUM_EQ_GENERAL_INVERSES
VSUM_EQ_NUMSEG
VSUM_EQ_SUPERSET
VSUM_GP
VSUM_GP_BASIC
VSUM_GP_MULTIPLIED
VSUM_GP_OFFSET
VSUM_GROUP
VSUM_IMAGE
VSUM_IMAGE_GEN
VSUM_IMAGE_NONZERO
VSUM_INCL_EXCL
VSUM_INJECTION
VSUM_LMUL
VSUM_NEG
VSUM_NONZERO_IMAGE_LEMMA
VSUM_NORM
VSUM_NORM_ALLSUBSETS_BOUND
VSUM_NORM_BOUND
VSUM_NORM_LE
VSUM_NORM_TRIANGLE
VSUM_OFFSET
VSUM_OFFSET_0
VSUM_OVER_TAGGED_DIVISION_LEMMA
VSUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA
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
valid_path
vec
vector_add
vector_angle
vector_derivative
vector_matrix_mul
vector_mul
vector_neg
vector_norm
vector_polynomial_function
vector_sub
vector_variation
vertices
vol_ball_wedge
vol_conic_cap_wedge
vol_conv
vol_frustt_wedge
vol_rect
vol_solid_triangle
volume_props
vsum