HOL html

Files Index

Theorems Index

B (theorems)

BABY_SARD
BAIRE
BAIRE_ALT
BALLOT
BALL_1
BALL_BIHOLOMORPHISM_EXISTS
BALL_BIHOLOMORPHISM_MOEBIUS_FUNCTION
BALL_DIST
BALL_DIST_CLOSED
BALL_EMPTY
BALL_EQ_EMPTY
BALL_INTERVAL
BALL_INTERVAL_0
BALL_LINEAR_IMAGE
BALL_MAX_UNION
BALL_MIN_INTER
BALL_NEIGH
BALL_OPEN
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
BDISJ_REPEATS_LEMMA
BEFORE_ABS
BEFORE_LBL
BEFORE_REL
BEPPO_LEVI_DECREASING
BEPPO_LEVI_INCREASING
BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING
BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE
BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING
BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE
BERNOULLI
BERNOULLI_1
BERNOULLI_1_0
BERNOULLI_ADD
BERNOULLI_ALT
BERNOULLI_BOUND
BERNOULLI_EVEN_BOUND
BERNOULLI_HALF
BERNOULLI_NUMBER
BERNOULLI_NUMBER_ALT
BERNOULLI_NUMBER_EQ_0
BERNOULLI_NUMBER_ZERO
BERNOULLI_RAABE_2
BERNOULLI_REFLECT
BERNOULLI_SUB_ADD1
BERNOULLI_UNIQUE
BERNSTEIN_LEMMA
BERNSTEIN_POS
BERNSTEIN_WEIERSTRASS
BERTRAND
BESSEL_INEQUALITY
BETA_THM
BETA_correct
BETWEEN_ANGLE
BETWEEN_ANTISYM
BETWEEN_COLLINEAR_DIST_EQ
BETWEEN_COLLINEAR_MDIST_EQ
BETWEEN_DIST_LE
BETWEEN_DIST_LT
BETWEEN_DOT
BETWEEN_EXISTS_EXTENSION
BETWEEN_IMP_COLLINEAR
BETWEEN_IN_CONVEX_HULL
BETWEEN_IN_SEGMENT
BETWEEN_KLEINIFY_MOEBIUS
BETWEEN_LINEAR_IMAGE_EQ
BETWEEN_METRICAL
BETWEEN_MIDPOINT
BETWEEN_NORM
BETWEEN_NORM_LE
BETWEEN_NORM_LT
BETWEEN_REFL
BETWEEN_REFL_EQ
BETWEEN_SYM
BETWEEN_THM
BETWEEN_TRANS
BETWEEN_TRANSLATION
BETWEEN_TRANS_2
BEZOUT
BEZOUT_ADD
BEZOUT_ADD_STRONG
BEZOUT_GCD
BEZOUT_GCD_POW
BEZOUT_GCD_STRONG
BEZOUT_LEMMA
BEZOUT_PRIME
BIDIFFERENTIABLE_FOURIER_CONVERGENCE_PERIODIC
BIGGER_PRIME_EXISTS
BIG_BERTRAND
BIG_POWER_LEMMA
BIJ
BIJECTIONS_CARD_EQ
BIJECTIONS_HAS_SIZE
BIJECTIONS_HAS_SIZE_EQ
BIJECTIVE_INJECTIVE_SURJECTIVE
BIJECTIVE_INVERSES
BIJECTIVE_LEFT_RIGHT_INVERSE
BIJECTIVE_ON_LEFT_RIGHT_INVERSE
BIJ_CARD
BIJ_INVERSE
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
BINARYSUM_BITSET
BINARYSUM_BOUND
BINARYSUM_BOUND_EQ
BINARYSUM_BOUND_LEMMA
BINARYSUM_DIV
BINARYSUM_DIV_DIVISIBLE
BINARY_BOUND
BINARY_DIV_POW2
BINARY_INDUCT
BINARY_INFERENCE_RULE
BINARY_PLUS_DIV_POW2
BINARY_UNIQUE_LEMMA
BINOM
BINOMIALISH_LEMMA
BINOMIAL_LEMMA
BINOMIAL_LEMMA_LT
BINOMIAL_THEOREM
BINOMIAL_TRIVIALITY
BINOM_0
BINOM_1
BINOM_BOTH_STEP
BINOM_BOTH_STEP_DOWN
BINOM_BOTH_STEP_REAL
BINOM_BOTTOM_STEP
BINOM_BOTTOM_STEP_REAL
BINOM_EQ_0
BINOM_EXPLICIT
BINOM_FACT
BINOM_GE_TOP
BINOM_INDUCT
BINOM_LT
BINOM_MUL_SHIFT
BINOM_PENULT
BINOM_REFL
BINOM_SYM
BINOM_TOP_STEP
BINOM_TOP_STEP_REAL
BIRTHDAY_THM
BIRTHDAY_THM_EXPLICIT
BIT0
BIT0_THM
BIT1
BIT1_DEF
BIT1_THM
BITSET_0
BITSET_BINARYSUM
BITSET_BOUND
BITSET_BOUND_EQ
BITSET_BOUND_LEMMA
BITSET_BOUND_WEAK
BITSET_EQ
BITSET_EQ_EMPTY
BITSET_STEP
BLAHBLAH
BLAHBLAH3
BLICHFELDT
BLOCH
BLOCH_COROLLARY
BLOCH_LEMMA
BLOCH_UNIT
BOLZANO_LEMMA
BOLZANO_LEMMA_ALT
BOLZANO_WEIERSTRASS
BOLZANO_WEIERSTRASS_COMPLEX_DISC
BOLZANO_WEIERSTRASS_CONTRAPOS
BOLZANO_WEIERSTRASS_IMP_BOUNDED
BOLZANO_WEIERSTRASS_IMP_CLOSED
BOOLEAN_EQ
BOOLEAN_EQ_TRUE
BOOLEAN_IN_BOOLSET
BOOL_CASES_AX
BORSUKIAN_ALT
BORSUKIAN_CIRCLE
BORSUKIAN_CIRCLE_ALT
BORSUKIAN_CLOSED_UNION
BORSUKIAN_COMPONENTWISE
BORSUKIAN_COMPONENTWISE_EQ
BORSUKIAN_CONTINUOUS_LOGARITHM
BORSUKIAN_CONTINUOUS_LOGARITHM_CIRCLE
BORSUKIAN_CONTINUOUS_LOGARITHM_CIRCLE_CX
BORSUKIAN_EMPTY
BORSUKIAN_EQ_SIMPLY_CONNECTED
BORSUKIAN_IMP_UNICOHERENT
BORSUKIAN_INJECTIVE_LINEAR_IMAGE
BORSUKIAN_MONOTONE_IMAGE_COMPACT
BORSUKIAN_OPEN_MAP_IMAGE_COMPACT
BORSUKIAN_OPEN_UNION
BORSUKIAN_RETRACTION_GEN
BORSUKIAN_SEPARATION_COMPACT
BORSUKIAN_SEPARATION_OPEN_CLOSED
BORSUKIAN_SPHERE
BORSUKIAN_TRANSLATION
BORSUKIAN_UNIV
BORSUK_HOMOTOPY_EXTENSION
BORSUK_HOMOTOPY_EXTENSION_HOMOTOPIC
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
BORSUK_ULAM
BOTTOM
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_COMPONENT_RETRACT_COMPLEMENT_MEETS
BOUNDED_CONIC_CAP
BOUNDED_CONIC_CAP_WEDGE
BOUNDED_CONV0
BOUNDED_CONVEX_HULL
BOUNDED_CONVEX_HULL_EQ
BOUNDED_DECREASING_CONVERGENT
BOUNDED_DIFF
BOUNDED_DIFFS
BOUNDED_DIFF_LOGMUL
BOUNDED_DIRICHLET_MANGOLDT_LEMMA
BOUNDED_DIRICHLET_MANGOLDT_NONPRINCIPAL
BOUNDED_DIRICHLET_MANGOLDT_NONZERO
BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL
BOUNDED_DIRICHLET_MANGOLDT_PRINCIPAL_LEMMA
BOUNDED_DIRICHLET_MANGOLDT_ZERO
BOUNDED_EMPTY
BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION
BOUNDED_EQ_BOLZANO_WEIERSTRASS
BOUNDED_FINITE
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_INTEGRALS_OVER_SUBINTERVALS
BOUNDED_INTER
BOUNDED_INTERIOR
BOUNDED_INTERS
BOUNDED_INTERVAL
BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT
BOUNDED_LFUNCTION_DIRICHLET_MANGOLDT_LEMMA
BOUNDED_LFUNCTION_PARTIAL_SUMS
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_SUM_OVER_DIRICHLET_CHARACTERS
BOUNDED_TRANSLATION
BOUNDED_TRANSLATION_EQ
BOUNDED_UNIFORMLY_CONTINUOUS_IMAGE
BOUNDED_UNION
BOUNDED_UNIONS
BOUNDED_UNIQUE_OUTSIDE
BOUNDED_VALID_PATH_IMAGE
BOUNDS_DIVIDED
BOUNDS_IGNORE
BOUNDS_LINEAR
BOUNDS_LINEAR_0
BOUNDS_NOTZERO
BOUND_LEMMA_0
BOUND_LEMMA_1
BOUND_LEMMA_2
BOUND_LEMMA_3
BOUND_LEMMA_4
BOUND_SN
BROUWER
BROUWER_ABSOLUTE_RETRACT
BROUWER_ABSOLUTE_RETRACT_GEN
BROUWER_AR
BROUWER_BALL
BROUWER_COMPACTNESS_LEMMA
BROUWER_CONTRACTIBLE_ANR
BROUWER_CUBE
BROUWER_FACTOR_THROUGH_AR
BROUWER_INESSENTIAL_ANR
BROUWER_REDUCTION_THEOREM
BROUWER_REDUCTION_THEOREM_GEN
BROUWER_SURJECTIVE
BROUWER_SURJECTIVE_CBALL
BROUWER_WEAK
BRUNN_MINKOWSKI_COMPACT
BRUNN_MINKOWSKI_CONVEX
BRUNN_MINKOWSKI_ELEMENTARY
BRUNN_MINKOWSKI_INTERVAL
BRUNN_MINKOWSKI_MEASURABLE
BRUNN_MINKOWSKI_OPEN
BSET_MIRROR
BUD_LEMMA
BUTLAST
BUTLAST_APPEND
BUTLAST_ID
BUTLAST_LENGTH
BUTLAST_NIL
BUTLAST_THM
BUTLAST_TL
Basic2move_THM
ball
ball_subset_ball
ball_symm
basis
bemma
bernoulli
bernoulli_number
bernpoly
bernstein
between
between_lemma
bicont_homeomorphism
bij_empty
bij_homeo
bij_imp_image
bij_inj_image
bij_sing
bij_target_set
bij_target_set_odd
bijection
bilinear
binarysum
binom
bitset
bool_INDUCT
bool_RECURSION
bool_cases
bool_size
bool_three_delete_bij
boolean
boolset
borsukian
bounded
bounded_avoidance_subset
bounded_diff
bounded_euclid
bounded_set_curve_cell_empty
bounded_subset_unions
bounded_triple_avoidance
bounded_triple_inner_union
bounded_unbounded_disj
bounded_unbounded_union
bracket
bset
bth