HOL html

Files Index

Theorems Index

D (theorems)

DECIMAL
DECOMPOSITION
DECREASING_BOUNDED_VARIATION
DECREASING_CLOSED_NEST
DECREASING_CLOSED_NEST_SING
DECREASING_LEFT_LIMIT
DECREASING_LEFT_LIMIT_1
DECREASING_LOG_OVER_N
DECREASING_RIGHT_LIMIT
DECREASING_RIGHT_LIMIT_1
DECREASING_VECTOR_VARIATION
DEDUCTION
DEDUCTION_LEMMA
DEDUCT_ANTISYM_RULE_correct
DEFINABLE_BY_ONEVAR
DEFINABLE_DEFINABLE_BY
DEFINABLE_ONEVAR
DEFINT_0
DEFINT_ADD
DEFINT_CMUL
DEFINT_COMBINE
DEFINT_CONST
DEFINT_DELTA
DEFINT_DELTA_LEFT
DEFINT_DELTA_RIGHT
DEFINT_EQ
DEFINT_FINITE_SPIKE
DEFINT_INTEGRAL
DEFINT_LE
DEFINT_NEG
DEFINT_POINT_SPIKE
DEFINT_SUB
DEFINT_TRIANGLE
DEFINT_WRONG
DEFSEQ_MINIMAL
DEFTRAJ_DEFSEQ
DEFTRAJ_MINIMAL
DEGREE_0
DEGREE_CONS
DEGREE_DELETE_EDGE
DEGREE_PNEG
DEGREE_SING
DEGREE_WELLDEF
DEGREE_ZERO
DELETE
DELETE1
DELETE1_APPEND
DELETE1_ID
DELETE1_LIST_UNIQ
DELETE1_REVPERM
DELETE_COMM
DELETE_DELETE
DELETE_EDGE_CLAUSES
DELETE_INSERT
DELETE_INTER
DELETE_NON_ELEMENT
DELETE_SUBSET
DELTA
DEMOIVRE
DENSE_ACCESSIBLE_FRONTIER_POINTS
DENSE_ACCESSIBLE_FRONTIER_POINTS_CONNECTED
DENSE_ACCESSIBLE_FRONTIER_POINT_PAIRS
DENUMERABLE_RATIONALS
DENUMERABLE_RATIONALS_EXPAND
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
DERANGEMENTS
DERANGEMENTS_EXP
DERANGEMENT_ADD1
DERANGEMENT_ADD2
DERANGEMENT_EMPTY
DERANGEMENT_INDUCT
DERANGEMENT_SING
DESARGUES_DIRECT
DESCARTES_RULE_OF_SIGNS
DEST_MK_MULTIVECTOR
DEST_MK_PAIR
DEST_PLANE_EQ
DEST_PLANE_NORM_LT
DEST_REC_INJ
DEST_VAR
DETERMINANT_AS_POLYFUN
DETERMINISM
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_TRANSPOSE
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
DIFF
DIFFERENCE_POS_LEMMA
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_FOURIER_CONVERGENCE_PERIODIC
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
DIFFS_EQUIV
DIFFS_LEMMA
DIFFS_LEMMA2
DIFFS_NEG
DIFF_ACS
DIFF_ACS_COMPOSITE
DIFF_ACS_SIN
DIFF_ADD
DIFF_ADD_CONST_COMMUTE
DIFF_ASN
DIFF_ASN_COMPOSITE
DIFF_ASN_COS
DIFF_ATN
DIFF_ATN_COMPOSITE
DIFF_BERNPOLY
DIFF_CARAT
DIFF_CHAIN
DIFF_CHAIN_AT
DIFF_CHAIN_TAN
DIFF_CHAIN_TAN_TANPOLYS
DIFF_CHAIN_WITHIN
DIFF_CMUL
DIFF_COMPOSITE
DIFF_CONST
DIFF_CONT
DIFF_COS
DIFF_DIFF
DIFF_DIFF2
DIFF_DIV
DIFF_EMPTY
DIFF_EQ_EMPTY
DIFF_EXP
DIFF_INSERT
DIFF_INTER
DIFF_INTERS
DIFF_INV
DIFF_INVERSE
DIFF_INVERSE_LT
DIFF_ISCONST
DIFF_ISCONST_ALL
DIFF_ISCONST_END
DIFF_ISCONST_END_SIMPLE
DIFF_LCONST
DIFF_LDEC
DIFF_LEMMA
DIFF_LINC
DIFF_LMAX
DIFF_LMIN
DIFF_LN
DIFF_LN_COMPOSITE
DIFF_MUL
DIFF_NEG
DIFF_POW
DIFF_SIN
DIFF_SQRT
DIFF_SQRT_COMPOSITE
DIFF_SQUARE
DIFF_SUB
DIFF_SUBSET
DIFF_SUM
DIFF_SURJ
DIFF_UNIONS
DIFF_UNIONS_NONEMPTY
DIFF_UNIQ
DIFF_UNIV
DIFF_X
DIFF_XM1
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_FINITE_IMAGE
DIMINDEX_FINITE_SUM
DIMINDEX_GE_1
DIMINDEX_HAS_SIZE_FINITE_SUM
DIMINDEX_MULTIVECTOR
DIMINDEX_NONZERO
DIMINDEX_UNIQUE
DIMINDEX_UNIV
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
DINT_UNIQ
DIOPH_CONJ
DIOPH_DISJ
DIOPH_EXP_LEMMA
DIOPH_LE
DIOPH_LT
DIOPH_NE
DIOPH_Y
DIRECTION_AXIOM_1
DIRECTION_AXIOM_2
DIRECTION_AXIOM_3
DIRECTION_AXIOM_4
DIRECTION_AXIOM_4_WEAK
DIRECTION_CLAUSES
DIRICHLET
DIRICHLET_CHARACTER_0
DIRICHLET_CHARACTER_1
DIRICHLET_CHARACTER_CHI_0
DIRICHLET_CHARACTER_CNJ
DIRICHLET_CHARACTER_CONG
DIRICHLET_CHARACTER_DISCRIMINATOR
DIRICHLET_CHARACTER_DIVISORSUM_EQ_1
DIRICHLET_CHARACTER_DIVISORSUM_POS
DIRICHLET_CHARACTER_DIVISORSUM_PRIMEPOW_POS
DIRICHLET_CHARACTER_EQ_0
DIRICHLET_CHARACTER_EQ_1
DIRICHLET_CHARACTER_EQ_PRINCIPAL
DIRICHLET_CHARACTER_GROUPINV
DIRICHLET_CHARACTER_GROUPMUL
DIRICHLET_CHARACTER_MUL
DIRICHLET_CHARACTER_MUL_CNJ
DIRICHLET_CHARACTER_NONPRINCIPAL
DIRICHLET_CHARACTER_NONPRINCIPAL_NONTRIVIAL
DIRICHLET_CHARACTER_NORM
DIRICHLET_CHARACTER_PERIODIC
DIRICHLET_CHARACTER_PERIODIC_GEN
DIRICHLET_CHARACTER_POW
DIRICHLET_CHARACTER_REAL_CASES
DIRICHLET_CHARACTER_ROOT
DIRICHLET_CHARACTER_SUM_MOD
DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS
DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_INEXPLICIT
DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_POS
DIRICHLET_CHARACTER_SUM_OVER_CHARACTERS_WEAK
DIRICHLET_CHARACTER_SUM_OVER_NUMBERS
DIRICHLET_CHARACTER_ZEROSUM
DIRICHLET_CHARACTER_ZEROSUM_MUL
DIRICHLET_KERNEL_0
DIRICHLET_KERNEL_CONTINUOUS
DIRICHLET_KERNEL_CONTINUOUS_STRONG
DIRICHLET_KERNEL_COSINE_SUM
DIRICHLET_KERNEL_NEG
DIRICHLET_MANGOLDT
DIRICHLET_MANGOLDT_EXPLICIT
DIRICHLET_STRONG
DISCRETE_BOUNDED_IMP_FINITE
DISCRETE_IMP_CLOSED
DISCRETE_IMP_COUNTABLE
DISJA
DISJA0
DISJA_S
DISJOINT
DISJOINT_AFFINE_HULL
DISJOINT_DELETE_SYM
DISJOINT_EMPTY
DISJOINT_EMPTY_REFL
DISJOINT_HYPERPLANE_CELLS
DISJOINT_HYPERPLANE_CELLS_EQ
DISJOINT_INSERT
DISJOINT_INTERVAL
DISJOINT_INTERVAL_1
DISJOINT_NUMSEG
DISJOINT_SYM
DISJOINT_UNION
DISJ_ACI
DISJ_ASSOC
DISJ_SYM
DISTANCE_ATTAINS_INF
DISTANCE_ATTAINS_SUP
DISTINCT_DISTINCT_OF_ODD
DISTINCT_OF_ODD
DISTINCT_OF_ODD_OF_DISTINCT
DISTINCT_PRIME_COPRIME
DISTINGUISHING_ROTATION_EXISTS
DISTINGUISHING_ROTATION_EXISTS_PAIR
DISTINGUISHING_ROTATION_EXISTS_POLYGON
DIST_0
DIST_CEXP_II_1
DIST_CLOSEST_POINT_LIPSCHITZ
DIST_ELIM_THM
DIST_EQ
DIST_EQ_0
DIST_FSTCART
DIST_INCREASES_ONLINE
DIST_LADD
DIST_LADD_0
DIST_LE_0
DIST_LE_CASES
DIST_LIFT
DIST_LMUL
DIST_LZERO
DIST_MIDPOINT
DIST_MUL
DIST_NZ
DIST_PASTECART_CANCEL
DIST_POS_LE
DIST_POS_LT
DIST_RADD
DIST_RADD_0
DIST_REAL
DIST_REFL
DIST_RMUL
DIST_RZERO
DIST_SCALING
DIST_SEGMENT_LEMMA
DIST_SNDCART
DIST_SYM
DIST_TRIANGLE
DIST_TRIANGLES_LE
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
DIVIDE
DIVIDES_0
DIVIDES_1
DIVIDES_2
DIVIDES_ADD
DIVIDES_ADD_REVL
DIVIDES_ADD_REVR
DIVIDES_ANTISYM
DIVIDES_BINOM_PRIME
DIVIDES_CASES
DIVIDES_CMUL2
DIVIDES_DEGREE
DIVIDES_DEGREE_LEMMA
DIVIDES_DIV
DIVIDES_DIVIDES_DIV
DIVIDES_DIV_MULT
DIVIDES_DIV_NOT
DIVIDES_EXP
DIVIDES_EXP2
DIVIDES_EXP_LE
DIVIDES_EXP_MINUS1
DIVIDES_EXP_PLUS1
DIVIDES_FACT
DIVIDES_FACT_PRIME
DIVIDES_GCD
DIVIDES_INT_OF_REAL_ADD
DIVIDES_LE
DIVIDES_LE_STRONG
DIVIDES_LMUL
DIVIDES_LMUL2
DIVIDES_LMUL2_EQ
DIVIDES_LNEG
DIVIDES_MOD
DIVIDES_MUL2
DIVIDES_MUL_L
DIVIDES_MUL_R
DIVIDES_NSUM
DIVIDES_ONE
DIVIDES_PRIMEPOW
DIVIDES_PRIME_EXP_LE
DIVIDES_PRIME_PRIME
DIVIDES_REFL
DIVIDES_REXP
DIVIDES_REXP_SUC
DIVIDES_RMUL
DIVIDES_RMUL2
DIVIDES_RMUL2_EQ
DIVIDES_RNEG
DIVIDES_SUB
DIVIDES_SUM_NOT_ZERO
DIVIDES_TRANS
DIVIDES_TRIVIAL_UPPERBOUND
DIVIDES_ZERO
DIVIDE_DIVIDE
DIVIDE_EQ
DIVIDE_PROD
DIVIDE_PROD2
DIVIDE_SUM
DIVIDE_SUMMAND
DIVISIBILITY_BY_3
DIVISION
DIVISION_0
DIVISION_1
DIVISION_APPEND
DIVISION_APPEND_EXPLICIT
DIVISION_APPEND_LEMMA1
DIVISION_APPEND_LEMMA2
DIVISION_APPEND_STRONG
DIVISION_BOUNDS
DIVISION_COMMON_POINT_BOUND
DIVISION_CONTAINS
DIVISION_DISJOINT_UNION
DIVISION_DOUBLESPLIT
DIVISION_DSIZE_EQ
DIVISION_DSIZE_EQ_ALT
DIVISION_DSIZE_GE
DIVISION_DSIZE_LE
DIVISION_EQ
DIVISION_EXISTS
DIVISION_GT
DIVISION_INTER
DIVISION_INTERMEDIATE
DIVISION_INTER_1
DIVISION_LBOUND
DIVISION_LBOUND_LT
DIVISION_LE
DIVISION_LE_SUC
DIVISION_LHS
DIVISION_LT
DIVISION_LT_GEN
DIVISION_MONO_LE
DIVISION_MONO_LE_SUC
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_RHS
DIVISION_SIMP
DIVISION_SINGLE
DIVISION_SPLIT
DIVISION_THM
DIVISION_UBOUND
DIVISION_UBOUND_LT
DIVISION_UNION_INTERVALS_EXISTS
DIVISORSUM_MOBIUS
DIVISORSUM_PRIMEPOW
DIVISORVSUM_PRIMEPOW
DIVMOD_ELIM_THM
DIVMOD_ELIM_THM'
DIVMOD_EXIST
DIVMOD_EXIST_0
DIVMOD_UNIQ
DIVMOD_UNIQ_LEMMA
DIV_ADD_MOD
DIV_DIV
DIV_EQ_0
DIV_EQ_EXCLUSION
DIV_EVEN
DIV_ID
DIV_LE
DIV_LE_EXCLUSION
DIV_LT
DIV_MOD
DIV_MONO
DIV_MONO2
DIV_MONO_LT
DIV_MULT2
DIV_MULT_ADD
DIV_MUL_LE
DIV_REFL
DIV_UNIQ
DO
DODECAHEDRON_CONGRUENT_EDGES
DODECAHEDRON_CONGRUENT_FACETS
DODECAHEDRON_EDGES
DODECAHEDRON_EDGES_PER_FACE
DODECAHEDRON_EDGES_PER_VERTEX
DODECAHEDRON_VERTICES
DOMAIN_EMPTY
DOMAIN_INSERT
DOMINATED_CONVERGENCE
DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE
DOMINATED_CONVERGENCE_INTEGRABLE
DORDER_LEMMA
DORDER_NGE
DORDER_TENDSTO
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
DOT_VECTOR
DOUBLE_THE_CUBE
DOUBLE_THE_CUBE_ALGEBRA
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
D_EUCLID_BOUND
DistinctImplies2moveable
d_euclid_bound2
d_euclid_cis
d_euclid_cis_ineq
d_euclid_eq_arg
d_euclid_floor
d_euclid_mk_segment
d_euclid_n
d_euclid_point
d_euclid_pointI_pos
d_euclid_pos
d_euclid_pos2
d_euclid_pow2
d_euclid_zero
d_euclidpq
def
definable
definable_by
defined_thm
defint
defseq
defth
deftraj
degree
degree4_vertex_hv
degree_vertex_annulus
degree_vertex_disk
degree_vertex_disk_ver2
delete_edge
delete_empty
delete_inters
delta_partition_lemma
delta_partition_lemma_ver2
delta_pos_arch
delta_x
dense_open
dense_subset
denumber
denumerable
dependent
depth
derangements
deranges
deriv
deriv2
dest_int_rep
dest_pt_point
det
det3
deterministic
diagonal_matrix
diagonalize
diameter
diff_pow1
diff_unchange
differentiable
differentiable_on
diffl
diffs
dihV
dim
dimindex
dirac_0
dirac_delta
dirichlet_character
dirichlet_kernel
disk_endpoint
disk_endpoint_gen
disk_endpoint_outer
dist
distinct_of_odd
distinctpairs
divides
divides_DELTA
division
division_of
division_points
domain
dorder
dot
dot_comm
dot_euclid
dot_linear
dot_linear2
dot_linear2_euclidean
dot_linear_euclidean
dot_lzero
dot_minus_linear
dot_minus_linear2
dot_minus_linear2_euclidean
dot_minus_linear_euclidean
dot_neg
dot_neg2
dot_nonneg
dot_point
dot_rzero
dot_scale
dot_scale2
dot_scale2_euclidean
dot_scale_euclidean
dot_updim
dot_zero
dot_zero_euclidean
drop
drop0
drop1
drop2
drop3
drop_ant_tac_example
droplevel
dropout
dsize
dth
dyadics_in_open_unit_interval