HOL html

Files Index

Theorems Index

B (theorems)

BABY_SARD
BALL_1
BALL_BIHOLOMORPHISM_EXISTS
BALL_BIHOLOMORPHISM_MOEBIUS_FUNCTION
BALL_EMPTY
BALL_EQ_EMPTY
BALL_INTERVAL
BALL_INTERVAL_0
BALL_LINEAR_IMAGE
BALL_MAX_UNION
BALL_MIN_INTER
BALL_SCALING
BALL_SUBSET_CBALL
BALL_SUBSET_OPEN_MAP_IMAGE
BALL_TRANSLATION
BALL_TRIVIAL
BALL_UNION_SPHERE
BANACH_FIX
BASIS_CARD_EQ_DIM
BASIS_COMPONENT
BASIS_COORDINATES_CONTINUOUS
BASIS_COORDINATES_LIPSCHITZ
BASIS_EQ_0
BASIS_EXISTS
BASIS_EXISTS_FINITE
BASIS_EXPANSION
BASIS_EXPANSION_UNIQUE
BASIS_HAS_SIZE_DIM
BASIS_HAS_SIZE_UNIV
BASIS_INJ
BASIS_INJ_EQ
BASIS_NE
BASIS_NONZERO
BASIS_ORTHOGONAL
BASIS_SUBSPACE_EXISTS
BEPPO_LEVI_DECREASING
BEPPO_LEVI_INCREASING
BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING
BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING
BERNSTEIN_LEMMA
BERNSTEIN_POS
BERNSTEIN_WEIERSTRASS
BESSEL_INEQUALITY
BETWEEN_ANGLE
BETWEEN_ANTISYM
BETWEEN_COLLINEAR_DIST_EQ
BETWEEN_DIST_LE
BETWEEN_DIST_LT
BETWEEN_DOT
BETWEEN_EXISTS_EXTENSION
BETWEEN_IMP_COLLINEAR
BETWEEN_IN_CONVEX_HULL
BETWEEN_IN_SEGMENT
BETWEEN_LINEAR_IMAGE_EQ
BETWEEN_MIDPOINT
BETWEEN_NORM
BETWEEN_NORM_LE
BETWEEN_NORM_LT
BETWEEN_REFL
BETWEEN_REFL_EQ
BETWEEN_SYM
BETWEEN_TRANS
BETWEEN_TRANSLATION
BETWEEN_TRANS_2
BILINEAR_BOUNDED
BILINEAR_BOUNDED_POS
BILINEAR_COMPLEX_MUL
BILINEAR_CONTINUOUS_COMPOSE
BILINEAR_CONTINUOUS_ON_COMPOSE
BILINEAR_CROSS
BILINEAR_DIFFERENTIABLE_AT_COMPOSE
BILINEAR_DIFFERENTIABLE_ON_COMPOSE
BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE
BILINEAR_DOT
BILINEAR_DROP_MUL
BILINEAR_EQ
BILINEAR_EQ_MBASIS
BILINEAR_EQ_STDBASIS
BILINEAR_GEOM
BILINEAR_INNER
BILINEAR_LADD
BILINEAR_LMUL
BILINEAR_LNEG
BILINEAR_LSUB
BILINEAR_LZERO
BILINEAR_OUTER
BILINEAR_PRODUCT
BILINEAR_RADD
BILINEAR_RMUL
BILINEAR_RNEG
BILINEAR_RSUB
BILINEAR_RZERO
BILINEAR_UNIFORMLY_CONTINUOUS_ON_COMPOSE
BILINEAR_VSUM
BILINEAR_VSUM_PARTIAL_PRE
BILINEAR_VSUM_PARTIAL_SUC
BLOCH
BLOCH_COROLLARY
BLOCH_LEMMA
BLOCH_UNIT
BOLZANO_WEIERSTRASS
BOLZANO_WEIERSTRASS_CONTRAPOS
BOLZANO_WEIERSTRASS_IMP_BOUNDED
BOLZANO_WEIERSTRASS_IMP_CLOSED
BORSUK_HOMOTOPY_EXTENSION
BORSUK_MAPS_HOMOTOPIC_IN_CONNECTED_COMPONENT_EQ
BORSUK_MAPS_HOMOTOPIC_IN_PATH_COMPONENT
BORSUK_MAP_ESSENTIAL_BOUNDED_COMPONENT
BORSUK_MAP_INTO_SPHERE
BORSUK_SEPARATION_THEOREM
BORSUK_SEPARATION_THEOREM_GEN
BOUNDED_ARC_IMAGE
BOUNDED_BALL
BOUNDED_CBALL
BOUNDED_CLOSED_CHAIN
BOUNDED_CLOSED_IMP_COMPACT
BOUNDED_CLOSED_INTERVAL
BOUNDED_CLOSED_NEST
BOUNDED_CLOSURE
BOUNDED_CLOSURE_EQ
BOUNDED_COMPONENTWISE
BOUNDED_CONIC_CAP
BOUNDED_CONIC_CAP_WEDGE
BOUNDED_CONV0
BOUNDED_CONVEX_HULL
BOUNDED_CONVEX_HULL_EQ
BOUNDED_DECREASING_CONVERGENT
BOUNDED_DIFF
BOUNDED_DIFFS
BOUNDED_EMPTY
BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION
BOUNDED_FRONTIER
BOUNDED_FUNCTIONS_BIJECTIONS_1
BOUNDED_FUNCTIONS_BIJECTIONS_2
BOUNDED_HALFSPACE_GE
BOUNDED_HALFSPACE_GT
BOUNDED_HALFSPACE_LE
BOUNDED_HALFSPACE_LT
BOUNDED_HAS_INF
BOUNDED_HAS_SUP
BOUNDED_HYPERPLANE_EQ_TRIVIAL
BOUNDED_INCREASING_CONVERGENT
BOUNDED_INSERT
BOUNDED_INSIDE
BOUNDED_INTER
BOUNDED_INTERIOR
BOUNDED_INTERS
BOUNDED_INTERVAL
BOUNDED_LIFT
BOUNDED_LINEAR_IMAGE
BOUNDED_LINEAR_IMAGE_EQ
BOUNDED_NEGATIONS
BOUNDED_PARTIAL_REAL_SUMS
BOUNDED_PARTIAL_SUMS
BOUNDED_PATH_IMAGE
BOUNDED_PCROSS
BOUNDED_PCROSS_EQ
BOUNDED_POS
BOUNDED_POS_LT
BOUNDED_RECTIFIABLE_PATH_IMAGE
BOUNDED_RELATIVE_FRONTIER
BOUNDED_SCALING
BOUNDED_SEGMENT
BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE
BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL
BOUNDED_SIMPLE_PATH_IMAGE
BOUNDED_SING
BOUNDED_SLICE
BOUNDED_SPHERE
BOUNDED_SUBSET
BOUNDED_SUBSET_BALL
BOUNDED_SUBSET_CBALL
BOUNDED_SUBSET_CLOSED_INTERVAL
BOUNDED_SUBSET_CLOSED_INTERVAL_SYMMETRIC
BOUNDED_SUBSET_OPEN_INTERVAL
BOUNDED_SUBSET_OPEN_INTERVAL_SYMMETRIC
BOUNDED_SUMS
BOUNDED_SUMS_IMAGE
BOUNDED_SUMS_IMAGES
BOUNDED_TRANSLATION
BOUNDED_TRANSLATION_EQ
BOUNDED_UNIFORMLY_CONTINUOUS_IMAGE
BOUNDED_UNION
BOUNDED_UNIONS
BOUNDED_UNIQUE_OUTSIDE
BOUNDED_VALID_PATH_IMAGE
BROUWER
BROUWER_BALL
BROUWER_COMPACTNESS_LEMMA
BROUWER_CONTRACTIBLE_ANR
BROUWER_CUBE
BROUWER_INESSENTIAL_ANR
BROUWER_REDUCTION_THEOREM
BROUWER_REDUCTION_THEOREM_GEN
BROUWER_SURJECTIVE
BROUWER_SURJECTIVE_CBALL
BROUWER_WEAK
ball
basis
bemma
bernstein
between
bilinear
bounded
bth