HOL html

Files Index

Theorems Index

D (theorems)

DECREASING_BOUNDED_VARIATION
DECREASING_CLOSED_NEST
DECREASING_CLOSED_NEST_SING
DECREASING_LEFT_LIMIT
DECREASING_LEFT_LIMIT_1
DECREASING_RIGHT_LIMIT
DECREASING_RIGHT_LIMIT_1
DECREASING_VECTOR_VARIATION
DEMOIVRE
DENSE_ACCESSIBLE_FRONTIER_POINTS
DENSE_ACCESSIBLE_FRONTIER_POINTS_CONNECTED
DENSE_ACCESSIBLE_FRONTIER_POINT_PAIRS
DEPENDENT_2
DEPENDENT_3
DEPENDENT_AFFINE_DEPENDENT_CASES
DEPENDENT_BIGGERSET
DEPENDENT_BIGGERSET_GENERAL
DEPENDENT_EXPLICIT
DEPENDENT_FINITE
DEPENDENT_IMP_AFFINE_DEPENDENT
DEPENDENT_LINEAR_IMAGE
DEPENDENT_LINEAR_IMAGE_EQ
DEPENDENT_MONO
DEPENDENT_SING
DEST_MK_MULTIVECTOR
DET_0
DET_1
DET_2
DET_3
DET_4
DET_CMUL
DET_COFACTOR
DET_COFACTOR_EXPANSION
DET_DEPENDENT_COLUMNS
DET_DEPENDENT_ROWS
DET_DIAGONAL
DET_EQ_0
DET_EQ_0_RANK
DET_I
DET_IDENTICAL_COLUMNS
DET_IDENTICAL_ROWS
DET_LINEAR_ROWS_VSUM
DET_LINEAR_ROWS_VSUM_LEMMA
DET_LINEAR_ROW_VSUM
DET_LOWERTRIANGULAR
DET_MATRIX_EQ_0
DET_MATRIX_EQ_0_LEFT
DET_MATRIX_EQ_0_RIGHT
DET_MATRIX_REFLECT_ALONG
DET_MATRIX_ROTATE2D
DET_MUL
DET_NEG
DET_ORTHOGONAL_MATRIX
DET_PERMUTE_COLUMNS
DET_PERMUTE_ROWS
DET_ROWS_MUL
DET_ROW_ADD
DET_ROW_MUL
DET_ROW_OPERATION
DET_ROW_SPAN
DET_TRANSP
DET_UPPERTRIANGULAR
DET_ZERO_COLUMN
DET_ZERO_ROW
DIAMETER_ATTAINED_FRONTIER
DIAMETER_ATTAINED_RELATIVE_FRONTIER
DIAMETER_BALL
DIAMETER_BOUNDED
DIAMETER_BOUNDED_BOUND
DIAMETER_BOUNDED_BOUND_LT
DIAMETER_CBALL
DIAMETER_CLOSURE
DIAMETER_COMPACT_ATTAINED
DIAMETER_CONVEX_HULL
DIAMETER_EMPTY
DIAMETER_EQ_0
DIAMETER_FRONTIER
DIAMETER_INTERVAL
DIAMETER_LE
DIAMETER_LINEAR_IMAGE
DIAMETER_POS_LE
DIAMETER_RELATIVE_FRONTIER
DIAMETER_SIMPLEX
DIAMETER_SING
DIAMETER_SPHERE
DIAMETER_SUBSET
DIAMETER_SUBSET_CBALL
DIAMETER_SUBSET_CBALL_NONEMPTY
DIAMETER_TRANSLATION
DIFFERENTIABLE_ADD
DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON
DIFFERENTIABLE_AT_LIFT_DOT2
DIFFERENTIABLE_AT_WITHIN
DIFFERENTIABLE_BOUND
DIFFERENTIABLE_CHAIN_AT
DIFFERENTIABLE_CHAIN_WITHIN
DIFFERENTIABLE_CMUL
DIFFERENTIABLE_COMPONENTWISE_AT
DIFFERENTIABLE_COMPONENTWISE_WITHIN
DIFFERENTIABLE_CONST
DIFFERENTIABLE_ID
DIFFERENTIABLE_IMP_CONTINUOUS_AT
DIFFERENTIABLE_IMP_CONTINUOUS_ON
DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN
DIFFERENTIABLE_IMP_PIECEWISE_DIFFERENTIABLE
DIFFERENTIABLE_LIFT_COMPONENT
DIFFERENTIABLE_LINEAR
DIFFERENTIABLE_MUL_AT
DIFFERENTIABLE_MUL_WITHIN
DIFFERENTIABLE_NEG
DIFFERENTIABLE_NORM_AT
DIFFERENTIABLE_ON_ADD
DIFFERENTIABLE_ON_COMPOSE
DIFFERENTIABLE_ON_CONST
DIFFERENTIABLE_ON_EMPTY
DIFFERENTIABLE_ON_EQ_DIFFERENTIABLE_AT
DIFFERENTIABLE_ON_ID
DIFFERENTIABLE_ON_IMP_PIECEWISE_DIFFERENTIABLE
DIFFERENTIABLE_ON_LIFT_DOT2
DIFFERENTIABLE_ON_LINEAR
DIFFERENTIABLE_ON_MUL
DIFFERENTIABLE_ON_NEG
DIFFERENTIABLE_ON_NORM
DIFFERENTIABLE_ON_REAL_POLYNOMIAL_FUNCTION
DIFFERENTIABLE_ON_SQNORM
DIFFERENTIABLE_ON_SUB
DIFFERENTIABLE_ON_SUBSET
DIFFERENTIABLE_ON_VECTOR_POLYNOMIAL_FUNCTION
DIFFERENTIABLE_REAL_POLYNOMIAL_FUNCTION_AT
DIFFERENTIABLE_SQNORM_AT
DIFFERENTIABLE_SUB
DIFFERENTIABLE_TRANSFORM_AT
DIFFERENTIABLE_TRANSFORM_WITHIN
DIFFERENTIABLE_VECTOR_POLYNOMIAL_FUNCTION
DIFFERENTIABLE_VSUM
DIFFERENTIABLE_VSUM_NUMSEG
DIFFERENTIABLE_WITHIN_LIFT_DOT2
DIFFERENTIABLE_WITHIN_OPEN
DIFFERENTIABLE_WITHIN_SUBSET
DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM
DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM
DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN
DIFFERENT_NORM_3_COLLINEAR_POINTS
DIFFS_AFFINE_HULL_SPAN
DIFF_CHAIN_AT
DIFF_CHAIN_WITHIN
DIHV
DIHV_ARCV
DIHV_EQ_0_PI_EQ_COPLANAR
DIHV_LINEAR_IMAGE
DIHV_NEG
DIHV_NEG_0
DIHV_RANGE
DIHV_SPECIAL_SCALE
DIHV_SYM
DIHV_TRANSLATION_EQ
DIMINDEX_MULTIVECTOR
DIM_CLOSURE
DIM_EMPTY
DIM_EQ_0
DIM_EQ_CARD
DIM_EQ_FULL
DIM_EQ_HYPERPLANE
DIM_EQ_SPAN
DIM_HYPERPLANE
DIM_IMAGE_KERNEL
DIM_IMAGE_KERNEL_GEN
DIM_INJECTIVE_LINEAR_IMAGE
DIM_INSERT
DIM_INSERT_0
DIM_KERNEL_COMPOSE
DIM_LE_CARD
DIM_LINEAR_IMAGE_LE
DIM_OPEN
DIM_OPEN_IN
DIM_ORTHOGONAL_SUM
DIM_PCROSS
DIM_PCROSS_STRONG
DIM_PSUBSET
DIM_ROWS_LE_DIM_COLUMNS
DIM_SING
DIM_SPAN
DIM_SPECIAL_HYPERPLANE
DIM_SPECIAL_SUBSPACE
DIM_SUBSET
DIM_SUBSET_UNIV
DIM_SUBSPACE_ORTHOGONAL_TO_VECTORS
DIM_SUBSTANDARD
DIM_SUMS_INTER
DIM_UNIQUE
DIM_UNIV
DINI
DISCRETE_BOUNDED_IMP_FINITE
DISCRETE_IMP_CLOSED
DISCRETE_IMP_COUNTABLE
DISJOINT_AFFINE_HULL
DISJOINT_INTERVAL
DISJOINT_INTERVAL_1
DISTANCE_ATTAINS_INF
DISTANCE_ATTAINS_SUP
DIST_0
DIST_CEXP_II_1
DIST_CLOSEST_POINT_LIPSCHITZ
DIST_EQ
DIST_EQ_0
DIST_FSTCART
DIST_INCREASES_ONLINE
DIST_LE_0
DIST_LIFT
DIST_MIDPOINT
DIST_MUL
DIST_NZ
DIST_PASTECART_CANCEL
DIST_POS_LE
DIST_POS_LT
DIST_REAL
DIST_REFL
DIST_SCALING
DIST_SNDCART
DIST_SYM
DIST_TRIANGLE
DIST_TRIANGLE_ADD
DIST_TRIANGLE_ADD_HALF
DIST_TRIANGLE_ALT
DIST_TRIANGLE_EQ
DIST_TRIANGLE_HALF_L
DIST_TRIANGLE_HALF_R
DIST_TRIANGLE_LE
DIST_TRIANGLE_LT
DIVISION_COMMON_POINT_BOUND
DIVISION_CONTAINS
DIVISION_DISJOINT_UNION
DIVISION_DOUBLESPLIT
DIVISION_INTER
DIVISION_INTER_1
DIVISION_OF
DIVISION_OF_AFFINITY
DIVISION_OF_CLOSED
DIVISION_OF_CONTENT_0
DIVISION_OF_FINITE
DIVISION_OF_NONTRIVIAL
DIVISION_OF_REFLECT
DIVISION_OF_SELF
DIVISION_OF_SING
DIVISION_OF_SUBSET
DIVISION_OF_TAGGED_DIVISION
DIVISION_OF_TRANSLATION
DIVISION_OF_TRIVIAL
DIVISION_OF_UNIONS
DIVISION_OF_UNION_SELF
DIVISION_POINTS_FINITE
DIVISION_POINTS_PSUBSET
DIVISION_POINTS_SUBSET
DIVISION_SPLIT
DIVISION_UNION_INTERVALS_EXISTS
DOMINATED_CONVERGENCE
DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE
DOMINATED_CONVERGENCE_INTEGRABLE
DOT_1
DOT_2
DOT_3
DOT_4
DOT_BASIS
DOT_BASIS_BASIS
DOT_BASIS_BASIS_UNEQUAL
DOT_CAUCHY_SCHWARZ_EQUAL
DOT_CROSS
DOT_CROSS_DET
DOT_CROSS_SELF
DOT_DROPOUT
DOT_EQ_0
DOT_LADD
DOT_LMUL
DOT_LMUL_MATRIX
DOT_LNEG
DOT_LSUB
DOT_LSUM
DOT_LZERO
DOT_MATRIX_PRODUCT
DOT_MATRIX_VECTOR_MUL
DOT_NORM
DOT_NORM_NEG
DOT_NORM_SUB
DOT_PASTECART
DOT_POS_LE
DOT_POS_LT
DOT_PUSHIN
DOT_RADD
DOT_RMUL
DOT_RNEG
DOT_ROWVECTOR_COLUMNVECTOR
DOT_RSUB
DOT_RSUM
DOT_RZERO
DOT_SCALING
DOT_SQUARE_NORM
DOT_SYM
DROPOUT_0
DROPOUT_ADD
DROPOUT_BASIS_3
DROPOUT_EQ
DROPOUT_GALOIS
DROPOUT_MUL
DROPOUT_PUSHIN
DROPOUT_SUB
DROP_ADD
DROP_CMUL
DROP_DIFFERENTIAL_NEG_AT_MAXIMUM
DROP_DIFFERENTIAL_POS_AT_MINIMUM
DROP_EQ
DROP_EQ_0
DROP_INDICATOR
DROP_INDICATOR_ABS_LE_1
DROP_INDICATOR_LE_1
DROP_INDICATOR_POS_LE
DROP_IN_IMAGE_DROP
DROP_LAMBDA
DROP_NEG
DROP_SUB
DROP_VEC
DROP_VSUM
DROP_WLOG_LE
DSUM_BOUND
delta_x
dependent
det
diagonal_matrix
diameter
differentiable
differentiable_on
dihV
dim
dist
division_of
division_points
dot
drop
dropout
dyadics_in_open_unit_interval