HOL html

Files Index

Theorems Index

R (theorems)

RADON
RADON_EX_LEMMA
RADON_PARTITION
RADON_S_LEMMA
RADON_V_LEMMA
RANK_0
RANK_BOUND
RANK_DIM_IM
RANK_EQ_0
RANK_GRAM
RANK_I
RANK_MUL_LE_LEFT
RANK_MUL_LE_RIGHT
RANK_NULLSPACE
RANK_ROW
RANK_SYLVESTER
RANK_TRANSP
RANK_TRIANGLE
RAY_TO_FRONTIER
RAY_TO_RELATIVE_FRONTIER
RCONE_GE_GT
RCONE_GT_GE
RCONE_GT_NEG
RE
REAL
REALLIM
REALLIM_1_OVER_LOG
REALLIM_1_OVER_N
REALLIM_ABS
REALLIM_ADD
REALLIM_AT
REALLIM_ATREAL
REALLIM_ATREAL_AT
REALLIM_ATREAL_ID
REALLIM_ATREAL_WITHINREAL
REALLIM_AT_INFINITY
REALLIM_AT_NEGINFINITY
REALLIM_AT_POSINFINITY
REALLIM_COMPLEX
REALLIM_CONG_AT
REALLIM_CONG_ATREAL
REALLIM_CONG_WITHIN
REALLIM_CONG_WITHINREAL
REALLIM_CONST
REALLIM_CONST_EQ
REALLIM_CONTINUOUS_FUNCTION
REALLIM_DIV
REALLIM_EVENTUALLY
REALLIM_IM
REALLIM_INV
REALLIM_LBOUND
REALLIM_LE
REALLIM_LMUL
REALLIM_LMUL_EQ
REALLIM_LOG_OVER_N
REALLIM_MAX
REALLIM_MIN
REALLIM_MUL
REALLIM_NEG
REALLIM_NEG_EQ
REALLIM_NULL
REALLIM_NULL_ABS
REALLIM_NULL_ADD
REALLIM_NULL_COMPARISON
REALLIM_NULL_LMUL
REALLIM_NULL_LMUL_EQ
REALLIM_NULL_POW
REALLIM_NULL_POW_EQ
REALLIM_NULL_RMUL
REALLIM_NULL_RMUL_EQ
REALLIM_POSINFINITY_SEQUENTIALLY
REALLIM_POW
REALLIM_POWN
REALLIM_RE
REALLIM_REAL_CONTINUOUS_FUNCTION
REALLIM_RMUL
REALLIM_RMUL_EQ
REALLIM_RPOW
REALLIM_SEQUENTIALLY
REALLIM_SUB
REALLIM_SUM
REALLIM_TRANSFORM
REALLIM_TRANSFORM_BOUND
REALLIM_TRANSFORM_EQ
REALLIM_TRANSFORM_EVENTUALLY
REALLIM_TRANSFORM_STRADDLE
REALLIM_TRANSFORM_WITHINREAL_SET
REALLIM_TRANSFORM_WITHIN_SET
REALLIM_UBOUND
REALLIM_UNIQUE
REALLIM_WITHIN
REALLIM_WITHINREAL
REALLIM_WITHINREAL_ID
REALLIM_WITHINREAL_LE
REALLIM_WITHINREAL_SUBSET
REALLIM_WITHINREAL_WITHIN
REALLIM_WITHIN_LE
REALLIM_WITHIN_OPEN
REALLIM_WITHIN_REAL_OPEN
REALLIM_WITHIN_SUBSET
REALLIM_ZERO_NEGINFINITY
REALLIM_ZERO_POSINFINITY
REAL_ABEL_LEMMA
REAL_ABEL_LIMIT_THEOREM
REAL_ABS_EXP
REAL_ABS_INFNORM
REAL_ABS_NORM
REAL_ABS_PI
REAL_ABS_RPOW
REAL_ABS_SUB_INFNORM
REAL_ABS_SUB_NORM
REAL_ACS
REAL_ADD
REAL_ADD_ARG
REAL_ADD_COS
REAL_ADD_SIN
REAL_ADD_TAN
REAL_AFFINITY_EQ
REAL_AFFINITY_LE
REAL_AFFINITY_LT
REAL_ANTIDERIVATIVE_CONTINUOUS
REAL_ANTIDERIVATIVE_INTEGRAL_CONTINUOUS
REAL_ARCH_INV
REAL_ARCH_POW
REAL_ARCH_POW2
REAL_ARCH_POW_INV
REAL_ARCH_RDIV_EQ_0
REAL_ASN
REAL_BEPPO_LEVI_DECREASING
REAL_BEPPO_LEVI_INCREASING
REAL_BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING
REAL_BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING
REAL_BOUNDED
REAL_BOUNDED_POS
REAL_BOUNDED_POS_LT
REAL_BOUNDED_REAL_INTERVAL
REAL_BOUNDED_SUBSET
REAL_BOUNDED_UNION
REAL_CLOSED
REAL_CLOSED_DIFF
REAL_CLOSED_EMPTY
REAL_CLOSED_HALFSPACE_GE
REAL_CLOSED_HALFSPACE_LE
REAL_CLOSED_IN
REAL_CLOSED_INTER
REAL_CLOSED_INTERS
REAL_CLOSED_OPEN_INTERVAL
REAL_CLOSED_REAL_INTERVAL
REAL_CLOSED_UNION
REAL_CLOSED_UNIONS
REAL_CLOSED_UNIV
REAL_CNJ
REAL_COMPACT_ATTAINS_INF
REAL_COMPACT_ATTAINS_SUP
REAL_COMPACT_CONTINUOUS_IMAGE
REAL_COMPACT_EQ_BOUNDED_CLOSED
REAL_COMPACT_IMP_BOUNDED
REAL_COMPACT_IMP_CLOSED
REAL_COMPACT_INTERVAL
REAL_COMPACT_UNIFORMLY_CONTINUOUS
REAL_COMPACT_UNION
REAL_COMPLEX_CONTINUOUS_ATREAL
REAL_COMPLEX_CONTINUOUS_WITHINREAL
REAL_COMPLEX_MEASURABLE_ON
REAL_CONTINUOUS_ABS
REAL_CONTINUOUS_ADD
REAL_CONTINUOUS_ADDITIVE_EXTEND
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR
REAL_CONTINUOUS_ADDITIVE_IMP_LINEAR_INTERVAL
REAL_CONTINUOUS_AT
REAL_CONTINUOUS_ATREAL
REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE
REAL_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE
REAL_CONTINUOUS_ATREAL_SQRT_COMPOSE
REAL_CONTINUOUS_ATREAL_WITHINREAL
REAL_CONTINUOUS_ATTAINS_INF
REAL_CONTINUOUS_ATTAINS_SUP
REAL_CONTINUOUS_AT_ACS
REAL_CONTINUOUS_AT_ARG
REAL_CONTINUOUS_AT_ASN
REAL_CONTINUOUS_AT_ATN
REAL_CONTINUOUS_AT_AZIM
REAL_CONTINUOUS_AT_AZIM_COMPOSE
REAL_CONTINUOUS_AT_AZIM_SHARP
REAL_CONTINUOUS_AT_COMPONENT
REAL_CONTINUOUS_AT_COMPOSE
REAL_CONTINUOUS_AT_COS
REAL_CONTINUOUS_AT_DIHV
REAL_CONTINUOUS_AT_DIHV_COMPOSE
REAL_CONTINUOUS_AT_EXP
REAL_CONTINUOUS_AT_ID
REAL_CONTINUOUS_AT_LINEAR_IMAGE
REAL_CONTINUOUS_AT_LOG
REAL_CONTINUOUS_AT_RPOW
REAL_CONTINUOUS_AT_SIN
REAL_CONTINUOUS_AT_SQRT
REAL_CONTINUOUS_AT_SQRT_COMPOSE
REAL_CONTINUOUS_AT_TAN
REAL_CONTINUOUS_AT_TRANSLATION
REAL_CONTINUOUS_AT_VECTOR_ANGLE
REAL_CONTINUOUS_AT_WITHIN
REAL_CONTINUOUS_COMPLEX_COMPONENTS_AT
REAL_CONTINUOUS_COMPLEX_COMPONENTS_WITHIN
REAL_CONTINUOUS_CONST
REAL_CONTINUOUS_CONTINUOUS
REAL_CONTINUOUS_CONTINUOUS1
REAL_CONTINUOUS_CONTINUOUS_ATREAL
REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_AT_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_CONTINUOUS_WITHINREAL_COMPOSE
REAL_CONTINUOUS_CONTINUOUS_WITHIN_COMPOSE
REAL_CONTINUOUS_DIST_AT
REAL_CONTINUOUS_DIST_WITHIN
REAL_CONTINUOUS_DIV
REAL_CONTINUOUS_DIV_AT
REAL_CONTINUOUS_DIV_ATREAL
REAL_CONTINUOUS_DIV_WITHIN
REAL_CONTINUOUS_DIV_WITHINREAL
REAL_CONTINUOUS_FLOOR
REAL_CONTINUOUS_FRAC
REAL_CONTINUOUS_IMP_REAL_MEASURABLE_ON_CLOSED_SUBSET
REAL_CONTINUOUS_INJECTIVE_IFF_MONOTONIC
REAL_CONTINUOUS_INV
REAL_CONTINUOUS_INV_AT
REAL_CONTINUOUS_INV_ATREAL
REAL_CONTINUOUS_INV_WITHIN
REAL_CONTINUOUS_INV_WITHINREAL
REAL_CONTINUOUS_LMUL
REAL_CONTINUOUS_MAX
REAL_CONTINUOUS_MEASURE_IN_HALFSPACE_LE
REAL_CONTINUOUS_MIN
REAL_CONTINUOUS_MUL
REAL_CONTINUOUS_NEG
REAL_CONTINUOUS_NORM_AT
REAL_CONTINUOUS_NORM_WITHIN
REAL_CONTINUOUS_ON
REAL_CONTINUOUS_ON_ACS
REAL_CONTINUOUS_ON_ADD
REAL_CONTINUOUS_ON_ASN
REAL_CONTINUOUS_ON_ATN
REAL_CONTINUOUS_ON_CASES
REAL_CONTINUOUS_ON_CASES_OPEN
REAL_CONTINUOUS_ON_COMPOSE
REAL_CONTINUOUS_ON_COMPOSE_FRAC
REAL_CONTINUOUS_ON_CONST
REAL_CONTINUOUS_ON_CONST_DYADIC_RATIONALS
REAL_CONTINUOUS_ON_COS
REAL_CONTINUOUS_ON_EQ
REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN
REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT
REAL_CONTINUOUS_ON_EXP
REAL_CONTINUOUS_ON_ID
REAL_CONTINUOUS_ON_INVERSE
REAL_CONTINUOUS_ON_INVERSE_ALT
REAL_CONTINUOUS_ON_LMUL
REAL_CONTINUOUS_ON_LOG
REAL_CONTINUOUS_ON_MUL
REAL_CONTINUOUS_ON_NEG
REAL_CONTINUOUS_ON_POW
REAL_CONTINUOUS_ON_RMUL
REAL_CONTINUOUS_ON_RPOW
REAL_CONTINUOUS_ON_SIN
REAL_CONTINUOUS_ON_SQRT
REAL_CONTINUOUS_ON_SUB
REAL_CONTINUOUS_ON_SUBSET
REAL_CONTINUOUS_ON_SUM
REAL_CONTINUOUS_ON_TAN
REAL_CONTINUOUS_ON_UNION
REAL_CONTINUOUS_ON_UNION_OPEN
REAL_CONTINUOUS_POW
REAL_CONTINUOUS_REAL_CONTINUOUS_ATREAL
REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_REAL_POLYMONIAL_FUNCTION
REAL_CONTINUOUS_RMUL
REAL_CONTINUOUS_SUB
REAL_CONTINUOUS_TRIVIAL_LIMIT
REAL_CONTINUOUS_WITHIN
REAL_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE
REAL_CONTINUOUS_WITHINREAL_COMPOSE
REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE
REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE
REAL_CONTINUOUS_WITHINREAL_SUBSET
REAL_CONTINUOUS_WITHIN_ACS
REAL_CONTINUOUS_WITHIN_ACS_STRONG
REAL_CONTINUOUS_WITHIN_ASN
REAL_CONTINUOUS_WITHIN_ASN_STRONG
REAL_CONTINUOUS_WITHIN_ATN
REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE
REAL_CONTINUOUS_WITHIN_COMPOSE
REAL_CONTINUOUS_WITHIN_COS
REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE
REAL_CONTINUOUS_WITHIN_EXP
REAL_CONTINUOUS_WITHIN_ID
REAL_CONTINUOUS_WITHIN_LOG
REAL_CONTINUOUS_WITHIN_RPOW
REAL_CONTINUOUS_WITHIN_SIN
REAL_CONTINUOUS_WITHIN_SQRT
REAL_CONTINUOUS_WITHIN_SQRT_COMPOSE
REAL_CONTINUOUS_WITHIN_SQRT_STRONG
REAL_CONTINUOUS_WITHIN_SUBSET
REAL_CONTINUOUS_WITHIN_TAN
REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE
REAL_CONVERGENT_IMP_BOUNDED
REAL_CONVEX_ADD
REAL_CONVEX_BOUND2_LT
REAL_CONVEX_BOUND_LE
REAL_CONVEX_BOUND_LT
REAL_CONVEX_DISTANCE
REAL_CONVEX_LMUL
REAL_CONVEX_LOCAL_GLOBAL_MINIMUM
REAL_CONVEX_LOWER
REAL_CONVEX_ON
REAL_CONVEX_ON_ASYM
REAL_CONVEX_ON_CONTINUOUS
REAL_CONVEX_ON_DERIVATIVES
REAL_CONVEX_ON_DERIVATIVES_IMP
REAL_CONVEX_ON_DERIVATIVE_INCREASING
REAL_CONVEX_ON_DERIVATIVE_INCREASING_IMP
REAL_CONVEX_ON_DERIVATIVE_SECANT
REAL_CONVEX_ON_DERIVATIVE_SECANT_IMP
REAL_CONVEX_ON_EXP
REAL_CONVEX_ON_JENSEN
REAL_CONVEX_ON_LEFT_SECANT
REAL_CONVEX_ON_LEFT_SECANT_MUL
REAL_CONVEX_ON_RIGHT_SEQUENT
REAL_CONVEX_ON_RIGHT_SEQUENT_MUL
REAL_CONVEX_ON_RPOW
REAL_CONVEX_ON_SECANT_DERIVATIVE
REAL_CONVEX_ON_SECANT_DERIVATIVE_IMP
REAL_CONVEX_ON_SECOND_DERIVATIVE
REAL_CONVEX_ON_SUBSET
REAL_CONVEX_RMUL
REAL_COS
REAL_CX
REAL_DERIVATIVE_IVT_DECREASING
REAL_DERIVATIVE_IVT_INCREASING
REAL_DERIVATIVE_NEG_LEFT_MAXIMUM
REAL_DERIVATIVE_NEG_RIGHT_MINIMUM
REAL_DERIVATIVE_POS_LEFT_MINIMUM
REAL_DERIVATIVE_POS_RIGHT_MAXIMUM
REAL_DERIVATIVE_UNIQUE_ATREAL
REAL_DERIVATIVE_ZERO_MAXMIN
REAL_DIFFERENTIABLE_ADD
REAL_DIFFERENTIABLE_AT
REAL_DIFFERENTIABLE_ATREAL_WITHIN
REAL_DIFFERENTIABLE_AT_ACS
REAL_DIFFERENTIABLE_AT_ASN
REAL_DIFFERENTIABLE_AT_ATN
REAL_DIFFERENTIABLE_AT_COS
REAL_DIFFERENTIABLE_AT_EXP
REAL_DIFFERENTIABLE_AT_LOG
REAL_DIFFERENTIABLE_AT_RPOW
REAL_DIFFERENTIABLE_AT_SIN
REAL_DIFFERENTIABLE_AT_SQRT
REAL_DIFFERENTIABLE_AT_TAN
REAL_DIFFERENTIABLE_BOUND
REAL_DIFFERENTIABLE_CARATHEODORY_ATREAL
REAL_DIFFERENTIABLE_CARATHEODORY_WITHINREAL
REAL_DIFFERENTIABLE_COMPOSE_ATREAL
REAL_DIFFERENTIABLE_COMPOSE_WITHIN
REAL_DIFFERENTIABLE_CONST
REAL_DIFFERENTIABLE_DIV_ATREAL
REAL_DIFFERENTIABLE_DIV_WITHIN
REAL_DIFFERENTIABLE_EQ
REAL_DIFFERENTIABLE_ID
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_ATREAL
REAL_DIFFERENTIABLE_IMP_CONTINUOUS_WITHINREAL
REAL_DIFFERENTIABLE_INV_ATREAL
REAL_DIFFERENTIABLE_INV_WITHIN
REAL_DIFFERENTIABLE_MUL_ATREAL
REAL_DIFFERENTIABLE_MUL_WITHIN
REAL_DIFFERENTIABLE_NEG
REAL_DIFFERENTIABLE_ON_ADD
REAL_DIFFERENTIABLE_ON_COMPOSE
REAL_DIFFERENTIABLE_ON_CONST
REAL_DIFFERENTIABLE_ON_DIFFERENTIABLE
REAL_DIFFERENTIABLE_ON_DIV
REAL_DIFFERENTIABLE_ON_ID
REAL_DIFFERENTIABLE_ON_IMP_DIFFERENTIABLE_ATREAL
REAL_DIFFERENTIABLE_ON_IMP_DIFFERENTIABLE_WITHIN
REAL_DIFFERENTIABLE_ON_IMP_REAL_CONTINUOUS_ON
REAL_DIFFERENTIABLE_ON_INV
REAL_DIFFERENTIABLE_ON_MUL
REAL_DIFFERENTIABLE_ON_NEG
REAL_DIFFERENTIABLE_ON_POW
REAL_DIFFERENTIABLE_ON_REAL_OPEN
REAL_DIFFERENTIABLE_ON_SUB
REAL_DIFFERENTIABLE_ON_SUBSET
REAL_DIFFERENTIABLE_ON_SUM
REAL_DIFFERENTIABLE_POW_ATREAL
REAL_DIFFERENTIABLE_POW_WITHIN
REAL_DIFFERENTIABLE_SUB
REAL_DIFFERENTIABLE_TRANSFORM
REAL_DIFFERENTIABLE_TRANSFORM_ATREAL
REAL_DIFFERENTIABLE_TRANSFORM_WITHIN
REAL_DIFFERENTIABLE_WITHIN
REAL_DIFFERENTIABLE_WITHIN_ACS
REAL_DIFFERENTIABLE_WITHIN_ASN
REAL_DIFFERENTIABLE_WITHIN_ATN
REAL_DIFFERENTIABLE_WITHIN_COS
REAL_DIFFERENTIABLE_WITHIN_EXP
REAL_DIFFERENTIABLE_WITHIN_LOG
REAL_DIFFERENTIABLE_WITHIN_SIN
REAL_DIFFERENTIABLE_WITHIN_SQRT
REAL_DIFFERENTIABLE_WITHIN_SUBSET
REAL_DIFFERENTIABLE_WITHIN_TAN
REAL_DIFF_CHAIN_ATREAL
REAL_DIFF_CHAIN_WITHIN
REAL_DINI
REAL_DIV
REAL_DIV_SQRT
REAL_DOMINATED_CONVERGENCE
REAL_EQ_AFFINITY
REAL_EXISTS
REAL_EXP
REAL_EXP_0
REAL_EXP_ADD
REAL_EXP_ADD_MUL
REAL_EXP_BOUND_LEMMA
REAL_EXP_EQ_1
REAL_EXP_INJ
REAL_EXP_LE_X
REAL_EXP_LOG
REAL_EXP_LT_1
REAL_EXP_MONO_IMP
REAL_EXP_MONO_LE
REAL_EXP_MONO_LT
REAL_EXP_N
REAL_EXP_NEG
REAL_EXP_NEG_MUL
REAL_EXP_NEG_MUL2
REAL_EXP_NZ
REAL_EXP_POS_LE
REAL_EXP_POS_LT
REAL_EXP_SUB
REAL_EXP_SUM
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG
REAL_FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
REAL_HALF
REAL_IMP_CNJ
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_LEFT
REAL_INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT
REAL_INFSUM
REAL_INFSUM_0
REAL_INFSUM_ADD
REAL_INFSUM_COMPLEX
REAL_INFSUM_EQ
REAL_INFSUM_LMUL
REAL_INFSUM_NEG
REAL_INFSUM_RESTRICT
REAL_INFSUM_RMUL
REAL_INFSUM_SUB
REAL_INFSUM_UNIQUE
REAL_INTEGRABLE_0
REAL_INTEGRABLE_ADD
REAL_INTEGRABLE_AFFINITY
REAL_INTEGRABLE_COMBINE
REAL_INTEGRABLE_CONST
REAL_INTEGRABLE_CONTINUOUS
REAL_INTEGRABLE_DECREASING
REAL_INTEGRABLE_DECREASING_PRODUCT
REAL_INTEGRABLE_DECREASING_PRODUCT_UNIV
REAL_INTEGRABLE_EQ
REAL_INTEGRABLE_INCREASING
REAL_INTEGRABLE_INCREASING_PRODUCT
REAL_INTEGRABLE_INCREASING_PRODUCT_UNIV
REAL_INTEGRABLE_INTEGRAL
REAL_INTEGRABLE_LINEAR
REAL_INTEGRABLE_LMUL
REAL_INTEGRABLE_NEG
REAL_INTEGRABLE_ON
REAL_INTEGRABLE_ON_EMPTY
REAL_INTEGRABLE_ON_LITTLE_SUBINTERVALS
REAL_INTEGRABLE_ON_NULL
REAL_INTEGRABLE_ON_OPEN_INTERVAL
REAL_INTEGRABLE_ON_REFL
REAL_INTEGRABLE_ON_SUBINTERVAL
REAL_INTEGRABLE_ON_SUPERSET
REAL_INTEGRABLE_REFLECT
REAL_INTEGRABLE_RESTRICT_INTER
REAL_INTEGRABLE_RESTRICT_UNIV
REAL_INTEGRABLE_RMUL
REAL_INTEGRABLE_SPIKE
REAL_INTEGRABLE_SPIKE_FINITE
REAL_INTEGRABLE_SPIKE_INTERIOR
REAL_INTEGRABLE_SPIKE_SET
REAL_INTEGRABLE_SPIKE_SET_EQ
REAL_INTEGRABLE_STRADDLE
REAL_INTEGRABLE_STRETCH
REAL_INTEGRABLE_SUB
REAL_INTEGRABLE_SUBINTERVAL
REAL_INTEGRABLE_SUM
REAL_INTEGRABLE_UNIFORM_LIMIT
REAL_INTEGRAL
REAL_INTEGRAL_0
REAL_INTEGRAL_ABS_BOUND_INTEGRAL
REAL_INTEGRAL_ADD
REAL_INTEGRAL_COMBINE
REAL_INTEGRAL_CONST
REAL_INTEGRAL_EMPTY
REAL_INTEGRAL_EQ
REAL_INTEGRAL_EQ_0
REAL_INTEGRAL_EQ_HAS_INTEGRAL
REAL_INTEGRAL_HAS_REAL_DERIVATIVE
REAL_INTEGRAL_LBOUND
REAL_INTEGRAL_LE
REAL_INTEGRAL_LINEAR
REAL_INTEGRAL_LMUL
REAL_INTEGRAL_NEG
REAL_INTEGRAL_NULL
REAL_INTEGRAL_OPEN_INTERVAL
REAL_INTEGRAL_POS
REAL_INTEGRAL_REAL_MEASURE
REAL_INTEGRAL_REAL_MEASURE_UNIV
REAL_INTEGRAL_REFL
REAL_INTEGRAL_REFLECT
REAL_INTEGRAL_RESTRICT
REAL_INTEGRAL_RESTRICT_INTER
REAL_INTEGRAL_RESTRICT_UNIV
REAL_INTEGRAL_RMUL
REAL_INTEGRAL_SPIKE
REAL_INTEGRAL_SPIKE_SET
REAL_INTEGRAL_SUB
REAL_INTEGRAL_SUBSET_LE
REAL_INTEGRAL_SUM
REAL_INTEGRAL_UBOUND
REAL_INTEGRAL_UNIQUE
REAL_INTERVAL_EQ_EMPTY
REAL_INTERVAL_INTERVAL
REAL_INTERVAL_NE_EMPTY
REAL_INTERVAL_OPEN_SUBSET_CLOSED
REAL_INTERVAL_SING
REAL_INTERVAL_TRANSLATION
REAL_INV
REAL_INV_EQ
REAL_INV_RPOW
REAL_IVT_DECREASING
REAL_IVT_INCREASING
REAL_LEBESGUE_MEASURABLE
REAL_LEBESGUE_MEASURABLE_CLOSED
REAL_LEBESGUE_MEASURABLE_COMPACT
REAL_LEBESGUE_MEASURABLE_COMPL
REAL_LEBESGUE_MEASURABLE_COUNTABLE_INTERS
REAL_LEBESGUE_MEASURABLE_COUNTABLE_INTERS_EXPLICIT
REAL_LEBESGUE_MEASURABLE_COUNTABLE_UNIONS
REAL_LEBESGUE_MEASURABLE_COUNTABLE_UNIONS_EXPLICIT
REAL_LEBESGUE_MEASURABLE_DIFF
REAL_LEBESGUE_MEASURABLE_EMPTY
REAL_LEBESGUE_MEASURABLE_IFF_MEASURABLE
REAL_LEBESGUE_MEASURABLE_INTER
REAL_LEBESGUE_MEASURABLE_INTERS
REAL_LEBESGUE_MEASURABLE_INTERVAL
REAL_LEBESGUE_MEASURABLE_ON_SUBINTERVALS
REAL_LEBESGUE_MEASURABLE_OPEN
REAL_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
REAL_LEBESGUE_MEASURABLE_PREIMAGE_OPEN
REAL_LEBESGUE_MEASURABLE_UNION
REAL_LEBESGUE_MEASURABLE_UNIONS
REAL_LEBESGUE_MEASURABLE_UNIV
REAL_LE_ABS_SINH
REAL_LE_AFFINITY
REAL_LE_BETWEEN
REAL_LE_LSQRT
REAL_LE_ROOT
REAL_LE_RSQRT
REAL_LE_SETDIST
REAL_LE_SETDIST_EQ
REAL_LE_X_SINH
REAL_LIM
REAL_LIM_SEQUENTIALLY
REAL_LSQRT_LE
REAL_LT_AFFINITY
REAL_LT_BETWEEN
REAL_LT_LSQRT
REAL_LT_RSQRT
REAL_MAX_SUP
REAL_MEASURABLE
REAL_MEASURABLE_ALMOST
REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_ABSOLUTELY_INTEGRABLE
REAL_MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_INTEGRABLE
REAL_MEASURABLE_COMPACT
REAL_MEASURABLE_COUNTABLE_INTERS
REAL_MEASURABLE_COUNTABLE_UNIONS
REAL_MEASURABLE_COUNTABLE_UNIONS_BOUNDED
REAL_MEASURABLE_COUNTABLE_UNIONS_STRONG
REAL_MEASURABLE_DIFF
REAL_MEASURABLE_EMPTY
REAL_MEASURABLE_IMP_REAL_LEBESGUE_MEASURABLE
REAL_MEASURABLE_INNER_OUTER
REAL_MEASURABLE_INTER
REAL_MEASURABLE_MEASURABLE
REAL_MEASURABLE_NESTED_UNIONS
REAL_MEASURABLE_ON_0
REAL_MEASURABLE_ON_ABS
REAL_MEASURABLE_ON_ADD
REAL_MEASURABLE_ON_CASES
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_0
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET_0
REAL_MEASURABLE_ON_COMPOSE_CONTINUOUS_OPEN_INTERVAL
REAL_MEASURABLE_ON_CONST
REAL_MEASURABLE_ON_DECREASING
REAL_MEASURABLE_ON_DECREASING_UNIV
REAL_MEASURABLE_ON_DIV
REAL_MEASURABLE_ON_INCREASING
REAL_MEASURABLE_ON_INCREASING_UNIV
REAL_MEASURABLE_ON_INV
REAL_MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET
REAL_MEASURABLE_ON_LIMIT
REAL_MEASURABLE_ON_LMUL
REAL_MEASURABLE_ON_MAX
REAL_MEASURABLE_ON_MEASURABLE_SUBSET
REAL_MEASURABLE_ON_MIN
REAL_MEASURABLE_ON_MUL
REAL_MEASURABLE_ON_NEG
REAL_MEASURABLE_ON_NEG_EQ
REAL_MEASURABLE_ON_PREIMAGE_CLOSED
REAL_MEASURABLE_ON_PREIMAGE_CLOSED_INTERVAL
REAL_MEASURABLE_ON_PREIMAGE_OPEN
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_GE
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_GT
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_LE
REAL_MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_LT
REAL_MEASURABLE_ON_PREIMAGE_OPEN_INTERVAL
REAL_MEASURABLE_ON_RESTRICT
REAL_MEASURABLE_ON_RMUL
REAL_MEASURABLE_ON_SIMPLE_FUNCTION_LIMIT
REAL_MEASURABLE_ON_SPIKE_SET
REAL_MEASURABLE_ON_SUB
REAL_MEASURABLE_ON_UNIV
REAL_MEASURABLE_OPEN
REAL_MEASURABLE_REAL_INTEGRABLE
REAL_MEASURABLE_REAL_INTERVAL
REAL_MEASURABLE_REAL_MEASURE_EQ_0
REAL_MEASURABLE_REAL_MEASURE_POS_LT
REAL_MEASURABLE_REAL_NEGLIGIBLE_SYMDIFF
REAL_MEASURABLE_SCALING
REAL_MEASURABLE_SCALING_EQ
REAL_MEASURABLE_TRANSLATION
REAL_MEASURABLE_UNION
REAL_MEASURABLE_UNIONS
REAL_MEASURE_DIFF_SUBSET
REAL_MEASURE_DISJOINT_UNION
REAL_MEASURE_DISJOINT_UNIONS
REAL_MEASURE_DISJOINT_UNIONS_IMAGE
REAL_MEASURE_DISJOINT_UNIONS_IMAGE_STRONG
REAL_MEASURE_EMPTY
REAL_MEASURE_EQ_0
REAL_MEASURE_MEASURE
REAL_MEASURE_POS_LE
REAL_MEASURE_REAL_INTEGRAL
REAL_MEASURE_REAL_INTEGRAL_UNIV
REAL_MEASURE_REAL_INTERVAL
REAL_MEASURE_REAL_NEGLIGIBLE_SYMDIFF
REAL_MEASURE_REAL_NEGLIGIBLE_UNION
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS_IMAGE
REAL_MEASURE_REAL_NEGLIGIBLE_UNIONS_IMAGE_STRONG
REAL_MEASURE_SCALING
REAL_MEASURE_SUBSET
REAL_MEASURE_TRANSLATION
REAL_MEASURE_UNION
REAL_MEASURE_UNIONS_LE
REAL_MEASURE_UNIONS_LE_IMAGE
REAL_MEASURE_UNION_LE
REAL_MEASURE_UNIQUE
REAL_MIN_INF
REAL_MONOTONE_CONVERGENCE_DECREASING
REAL_MONOTONE_CONVERGENCE_INCREASING
REAL_MONOTONE_CONVERGENCE_INCREASING_AE
REAL_MUL
REAL_MUL_COS_COS
REAL_MUL_COS_SIN
REAL_MUL_CX
REAL_MUL_SIN_COS
REAL_MUL_SIN_SIN
REAL_MUL_SUM
REAL_MUL_SUM_NUMSEG
REAL_MVT
REAL_MVT_CAUCHY
REAL_MVT_SIMPLE
REAL_MVT_VERY_SIMPLE
REAL_NEG
REAL_NEGLIGIBLE_COUNTABLE
REAL_NEGLIGIBLE_COUNTABLE_UNIONS
REAL_NEGLIGIBLE_DIFF
REAL_NEGLIGIBLE_EMPTY
REAL_NEGLIGIBLE_FINITE
REAL_NEGLIGIBLE_FRONTIER_INTERVAL
REAL_NEGLIGIBLE_INSERT
REAL_NEGLIGIBLE_INTER
REAL_NEGLIGIBLE_ON_INTERVALS
REAL_NEGLIGIBLE_OUTER
REAL_NEGLIGIBLE_OUTER_LE
REAL_NEGLIGIBLE_REAL_INTERVAL
REAL_NEGLIGIBLE_SING
REAL_NEGLIGIBLE_SUBSET
REAL_NEGLIGIBLE_TRANSLATION
REAL_NEGLIGIBLE_TRANSLATION_EQ
REAL_NEGLIGIBLE_TRANSLATION_REV
REAL_NEGLIGIBLE_UNION
REAL_NEGLIGIBLE_UNIONS
REAL_NEGLIGIBLE_UNION_EQ
REAL_NORM
REAL_NORM_POS
REAL_OPEN
REAL_OPEN_CLOSED_INTERVAL
REAL_OPEN_DIFF
REAL_OPEN_EMPTY
REAL_OPEN_EXISTS_RATIONAL
REAL_OPEN_HALFSPACE_GT
REAL_OPEN_HALFSPACE_LT
REAL_OPEN_IN
REAL_OPEN_INTER
REAL_OPEN_INTERS
REAL_OPEN_RATIONAL
REAL_OPEN_REAL_CLOSED
REAL_OPEN_REAL_INTERVAL
REAL_OPEN_SET_EXISTS_RATIONAL
REAL_OPEN_SET_RATIONAL
REAL_OPEN_SUBREAL_OPEN
REAL_OPEN_UNION
REAL_OPEN_UNIONS
REAL_OPEN_UNIV
REAL_PARTIAL_SUMS_LE_INFSUM
REAL_POW
REAL_POWER_SERIES_CONV_IMP_ABSCONV
REAL_POW_LBOUND
REAL_POW_ROOT
REAL_ROLLE
REAL_ROLLE_SIMPLE
REAL_ROOT_DIV
REAL_ROOT_INV
REAL_ROOT_LE
REAL_ROOT_MUL
REAL_ROOT_POW
REAL_ROOT_RPOW
REAL_RSQRT_LE
REAL_SECOND_MEAN_VALUE_THEOREM
REAL_SECOND_MEAN_VALUE_THEOREM_BONNET
REAL_SECOND_MEAN_VALUE_THEOREM_BONNET_FULL
REAL_SECOND_MEAN_VALUE_THEOREM_FULL
REAL_SECOND_MEAN_VALUE_THEOREM_GEN
REAL_SECOND_MEAN_VALUE_THEOREM_GEN_FULL
REAL_SEGMENT
REAL_SEGMENT_INTERVAL
REAL_SEGMENT_SEGMENT
REAL_SEQ_OFFSET
REAL_SEQ_OFFSET_REV
REAL_SERIES
REAL_SERIES_0
REAL_SERIES_ABSCONV_IMP_CONV
REAL_SERIES_ADD
REAL_SERIES_CAUCHY
REAL_SERIES_CAUCHY_UNIFORM
REAL_SERIES_COMPARISON
REAL_SERIES_COMPARISON_UNIFORM
REAL_SERIES_DIFFS
REAL_SERIES_DIRICHLET
REAL_SERIES_FINITE
REAL_SERIES_FINITE_SUPPORT
REAL_SERIES_FROM
REAL_SERIES_GOESTOZERO
REAL_SERIES_LMUL
REAL_SERIES_NEG
REAL_SERIES_RATIO
REAL_SERIES_RESTRICT
REAL_SERIES_RMUL
REAL_SERIES_SUB
REAL_SERIES_SUBSET
REAL_SERIES_SUM
REAL_SERIES_TRIVIAL
REAL_SERIES_UNIQUE
REAL_SGN_IM_COMPLEX_DIV
REAL_SGN_RE_COMPLEX_DIV
REAL_SGN_SIN_AZIM
REAL_SIN
REAL_STEINHAUS
REAL_STONE_WEIERSTRASS
REAL_STONE_WEIERSTRASS_ALT
REAL_SUB
REAL_SUB_ARG
REAL_SUB_COS
REAL_SUB_SIN
REAL_SUB_TAN
REAL_SUMMABLE
REAL_SUMMABLE_0
REAL_SUMMABLE_ADD
REAL_SUMMABLE_COMPARISON
REAL_SUMMABLE_COMPLEX
REAL_SUMMABLE_EQ
REAL_SUMMABLE_EQ_COFINITE
REAL_SUMMABLE_EQ_EVENTUALLY
REAL_SUMMABLE_FROM_ELSEWHERE
REAL_SUMMABLE_GP
REAL_SUMMABLE_IFF
REAL_SUMMABLE_IFF_COFINITE
REAL_SUMMABLE_IFF_EVENTUALLY
REAL_SUMMABLE_IMP_BOUNDED
REAL_SUMMABLE_IMP_REAL_SUMS_BOUNDED
REAL_SUMMABLE_IMP_TOZERO
REAL_SUMMABLE_LMUL
REAL_SUMMABLE_NEG
REAL_SUMMABLE_RESTRICT
REAL_SUMMABLE_RMUL
REAL_SUMMABLE_SUB
REAL_SUMMABLE_SUBSET
REAL_SUMMABLE_TRIVIAL
REAL_SUMS
REAL_SUMS_COMPLEX
REAL_SUMS_EQ
REAL_SUMS_FINITE_DIFF
REAL_SUMS_FINITE_UNION
REAL_SUMS_GP
REAL_SUMS_IFF
REAL_SUMS_IM
REAL_SUMS_INFSUM
REAL_SUMS_LE2
REAL_SUMS_OFFSET
REAL_SUMS_OFFSET_REV
REAL_SUMS_RE
REAL_SUMS_REINDEX
REAL_SUMS_SUMMABLE
REAL_SUM_INTEGRAL_BOUNDS_DECREASING
REAL_SUM_INTEGRAL_BOUNDS_INCREASING
REAL_SUM_INTEGRAL_LBOUND_DECREASING
REAL_SUM_INTEGRAL_LBOUND_INCREASING
REAL_SUM_INTEGRAL_UBOUND_DECREASING
REAL_SUM_INTEGRAL_UBOUND_INCREASING
REAL_TAN
REAL_TAYLOR
REAL_TAYLOR_MVT_NEG
REAL_TAYLOR_MVT_POS
REAL_TENDSTO
REAL_TIETZE_PERIODIC_INTERVAL
REAL_UNIFORMLY_CONTINUOUS_IMP_REAL_CONTINUOUS
REAL_UNIFORMLY_CONTINUOUS_ON
REAL_UNIFORMLY_CONTINUOUS_ON_ADD
REAL_UNIFORMLY_CONTINUOUS_ON_COMPOSE
REAL_UNIFORMLY_CONTINUOUS_ON_CONST
REAL_UNIFORMLY_CONTINUOUS_ON_ID
REAL_UNIFORMLY_CONTINUOUS_ON_LMUL
REAL_UNIFORMLY_CONTINUOUS_ON_NEG
REAL_UNIFORMLY_CONTINUOUS_ON_RMUL
REAL_UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY
REAL_UNIFORMLY_CONTINUOUS_ON_SUB
REAL_UNIFORMLY_CONTINUOUS_ON_SUBSET
REAL_UNIFORMLY_CONTINUOUS_ON_SUM
REAL_VARIATION_AFFINITY
REAL_VARIATION_AFFINITY2
REAL_VARIATION_COMBINE
REAL_VARIATION_CONTINUOUS
REAL_VARIATION_CONTINUOUS_LEFT
REAL_VARIATION_CONTINUOUS_RIGHT
REAL_VARIATION_GE_ABS_FUNCTION
REAL_VARIATION_GE_FUNCTION
REAL_VARIATION_MINUS_FUNCTION_MONOTONE
REAL_VARIATION_MONOTONE
REAL_VARIATION_NEG
REAL_VARIATION_POS_LE
REAL_VARIATION_REFLECT
REAL_VARIATION_REFLECT2
REAL_VARIATION_REFLECT_INTERVAL
REAL_VARIATION_TRANSLATION
REAL_VARIATION_TRANSLATION2
REAL_VARIATION_TRANSLATION_INTERVAL
REAL_VARIATION_TRIANGLE
REAL_VSUM
RECTIFIABLE_PATH_DIFFERENTIABLE
RECTIFIABLE_PATH_IMP_PATH
RECTIFIABLE_PATH_JOIN
RECTIFIABLE_PATH_JOIN_EQ
RECTIFIABLE_PATH_JOIN_IMP
RECTIFIABLE_PATH_LINEPATH
RECTIFIABLE_PATH_REVERSEPATH
RECTIFIABLE_PATH_SUBPATH
RECTIFIABLE_VALID_PATH
RECT_INTERVAL
REDUCED_LABELLING
REDUCED_LABELLING_0
REDUCED_LABELLING_1
REDUCED_LABELLING_SUC
REDUCED_LABELLING_UNIQUE
REDUCE_LABELLING_0
REFLECT_ALONG_0
REFLECT_ALONG_1D
REFLECT_ALONG_ADD
REFLECT_ALONG_BASIS
REFLECT_ALONG_EQ_0
REFLECT_ALONG_EQ_SELF
REFLECT_ALONG_INVOLUTION
REFLECT_ALONG_LINEAR_IMAGE
REFLECT_ALONG_MUL
REFLECT_ALONG_REFL
REFLECT_ALONG_SCALE
REFLECT_ALONG_ZERO
REFLECT_INTERVAL
REFLECT_REAL_INTERVAL
RELATIVE_BOUNDARY_OF_CONVEX_HULL
RELATIVE_BOUNDARY_OF_POLYHEDRON
RELATIVE_BOUNDARY_OF_TRIANGLE
RELATIVE_BOUNDARY_RETRACT_OF_PUNCTURED_AFFINE_HULL
RELATIVE_FRONTIER_BALL
RELATIVE_FRONTIER_CBALL
RELATIVE_FRONTIER_CLOSURE
RELATIVE_FRONTIER_CONVEX_HULL_CASES
RELATIVE_FRONTIER_CONVEX_HULL_EXPLICIT
RELATIVE_FRONTIER_CONVEX_INTER_AFFINE
RELATIVE_FRONTIER_EMPTY
RELATIVE_FRONTIER_EQ_EMPTY
RELATIVE_FRONTIER_FRONTIER
RELATIVE_FRONTIER_INJECTIVE_LINEAR_IMAGE
RELATIVE_FRONTIER_NONEMPTY_INTERIOR
RELATIVE_FRONTIER_NOT_SING
RELATIVE_FRONTIER_OF_CONVEX_HULL
RELATIVE_FRONTIER_OF_POLYHEDRON
RELATIVE_FRONTIER_OF_POLYHEDRON_ALT
RELATIVE_FRONTIER_OF_TRIANGLE
RELATIVE_FRONTIER_RETRACT_OF_PUNCTURED_AFFINE_HULL
RELATIVE_FRONTIER_SING
RELATIVE_FRONTIER_TRANSLATION
RELATIVE_INTERIOR
RELATIVE_INTERIOR_AFFINE
RELATIVE_INTERIOR_CONVEX_CONTAINS_SAME_RAY
RELATIVE_INTERIOR_CONVEX_HULL_EXPLICIT
RELATIVE_INTERIOR_CONVEX_INTER_AFFINE
RELATIVE_INTERIOR_CONVEX_PROLONG
RELATIVE_INTERIOR_EMPTY
RELATIVE_INTERIOR_EQ
RELATIVE_INTERIOR_EQ_CLOSURE
RELATIVE_INTERIOR_EQ_EMPTY
RELATIVE_INTERIOR_INJECTIVE_LINEAR_IMAGE
RELATIVE_INTERIOR_INTERIOR
RELATIVE_INTERIOR_LINEAR_IMAGE_CONVEX
RELATIVE_INTERIOR_MAXIMAL
RELATIVE_INTERIOR_NONEMPTY_INTERIOR
RELATIVE_INTERIOR_OF_POLYHEDRON
RELATIVE_INTERIOR_OPEN
RELATIVE_INTERIOR_OPEN_IN
RELATIVE_INTERIOR_PCROSS
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT
RELATIVE_INTERIOR_PROLONG
RELATIVE_INTERIOR_SEGMENT
RELATIVE_INTERIOR_SING
RELATIVE_INTERIOR_SUBSET
RELATIVE_INTERIOR_TRANSLATION
RELATIVE_INTERIOR_UNBOUNDED_CONVEX_CONTAINS_RAY
RELATIVE_INTERIOR_UNBOUNDED_CONVEX_CONTAINS_RAYS
RELATIVE_INTERIOR_UNIQUE
RELATIVE_INTERIOR_UNIV
RETRACTION
RETRACTION_ARC
RETRACTION_IDEMPOTENT
RETRACTION_IMP_QUOTIENT_MAP
RETRACTION_REFL
RETRACTION_SUBSET
RETRACTION_o
RETRACT_FIXPOINT_PROPERTY
RETRACT_OF_CLOSED
RETRACT_OF_COHOMOTOPICALLY_TRIVIAL
RETRACT_OF_COHOMOTOPICALLY_TRIVIAL_NULL
RETRACT_OF_COMPACT
RETRACT_OF_CONNECTED
RETRACT_OF_CONTRACTIBLE
RETRACT_OF_EMPTY
RETRACT_OF_HOMOTOPICALLY_TRIVIAL
RETRACT_OF_HOMOTOPICALLY_TRIVIAL_NULL
RETRACT_OF_IMP_EXTENSIBLE
RETRACT_OF_IMP_SUBSET
RETRACT_OF_INJECTIVE_LINEAR_IMAGE
RETRACT_OF_LINEAR_IMAGE_EQ
RETRACT_OF_LOCALLY_COMPACT
RETRACT_OF_LOCALLY_CONNECTED
RETRACT_OF_LOCALLY_PATH_CONNECTED
RETRACT_OF_PATH_CONNECTED
RETRACT_OF_PCROSS
RETRACT_OF_REFL
RETRACT_OF_SIMPLY_CONNECTED
RETRACT_OF_SING
RETRACT_OF_SUBSET
RETRACT_OF_TRANS
RETRACT_OF_TRANSLATION
RETRACT_OF_TRANSLATION_EQ
REVERSEPATH_JOINPATHS
REVERSEPATH_LINEAR_IMAGE
REVERSEPATH_LINEPATH
REVERSEPATH_REVERSEPATH
REVERSEPATH_SUBPATH
REVERSEPATH_TRANSLATION
REVERSE_LINEAR_IMAGE
REVERSE_TRANSLATION
RE_ADD
RE_CACS
RE_CACS_BOUND
RE_CACS_BOUNDS
RE_CASN
RE_CASN_BOUND
RE_CASN_BOUNDS
RE_CATN_BOUNDS
RE_CCOS
RE_CEXP
RE_CLOG
RE_CLOG_POS_LE
RE_CLOG_POS_LT
RE_CLOG_POS_LT_IMP
RE_CMUL
RE_CNJ
RE_COMPLEX_DIV_EQ_0
RE_COMPLEX_DIV_GE_0
RE_COMPLEX_DIV_GT_0
RE_COMPLEX_DIV_LEMMA
RE_COMPLEX_DIV_LE_0
RE_COMPLEX_DIV_LT_0
RE_CSIN
RE_CSQRT
RE_CX
RE_DEF
RE_DIV_CX
RE_II
RE_LINEPATH_CX
RE_MUL_CX
RE_MUL_II
RE_NEG
RE_POS_SEGMENT
RE_POW_2
RE_SUB
RE_VSUM
RE_WINDING_NUMBER
RIEMANN_MAPPING_THEOREM
RIGHT_INVERSE_LINEAR
RIGHT_INVERTIBLE_TRANSP
RIGID_TRANSFORMATION_BETWEEN_2
RIGID_TRANSFORMATION_BETWEEN_3
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS
RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS_STRONG
ROLLE
ROOT_0
ROOT_1
ROOT_2
ROOT_EXP_LOG
ROOT_INJ
ROOT_MONO_LE
ROOT_MONO_LE_EQ
ROOT_MONO_LT
ROOT_MONO_LT_EQ
ROOT_POS_LE
ROOT_POS_LT
ROOT_UNIQUE
ROOT_WORKS
ROTATE2D_0
ROTATE2D_2PI
ROTATE2D_ADD
ROTATE2D_ADD_VECTORS
ROTATE2D_COMPLEX
ROTATE2D_EQ
ROTATE2D_EQ_0
ROTATE2D_NPI
ROTATE2D_PI
ROTATE2D_PI2
ROTATE2D_POLAR
ROTATE2D_SUB
ROTATE2D_SUB_ARG
ROTATE2D_ZERO
ROTATION_EXISTS
ROTATION_EXISTS_1
ROTATION_HORIZONTAL_LINE
ROTATION_HORIZONTAL_PLANE
ROTATION_LOWDIM_HORIZONTAL
ROTATION_MATRIX_2
ROTATION_MATRIX_EXISTS_BASIS
ROTATION_MATRIX_ROTATE2D
ROTATION_MATRIX_ROTATE2D_EQ
ROTATION_PLANE_HORIZONTAL
ROTATION_RIGHTWARD_LINE
ROTATION_ROTATE2D
ROTATION_ROTATE2D_EXISTS
ROTATION_ROTATE2D_EXISTS_GEN
ROTATION_ROTATE2D_EXISTS_ORTHOGONAL
ROTATION_ROTATE2D_EXISTS_ORTHOGONAL_ORIENTED
ROTHE
ROTOINVERSION_MATRIX_REFLECT_ALONG
ROWS_TRANSP
ROW_TRANSP
RPOW_1_LE
RPOW_ADD
RPOW_ADD_ALT
RPOW_EQ_0
RPOW_INV
RPOW_LE2
RPOW_LNEG
RPOW_LT2
RPOW_MONO
RPOW_MONO_INV
RPOW_MUL
RPOW_NEG
RPOW_ONE
RPOW_POS_LE
RPOW_POS_LT
RPOW_POW
RPOW_RPOW
RPOW_SQRT
RPOW_ZERO
RSUM_BOUND
RSUM_COMPONENT_LE
RSUM_DIFF_BOUND
rank
rcone_eq
rcone_ge
rcone_gt
rconesgn
real
real_bounded
real_closed
real_compact
real_continuous
real_continuous_at
real_continuous_atreal
real_continuous_on
real_continuous_within
real_continuous_withinreal
real_convex_on
real_derivative
real_differentiable
real_differentiable_on
real_infsum
real_integrable_on
real_integral
real_interval
real_lebesgue_measurable
real_measurable
real_measurable_on
real_measure
real_negligible
real_open
real_segment
real_summable
real_sums
real_uniformly_continuous_on
real_variation
reallim
rect
rectifiable_path
recursion_on_dyadic_rationals
recursion_on_dyadic_rationals_1
reduced
reflect_along
relative_frontier
relative_interior
retract_of
retraction
reversepath
reversion
root
rotate2d
rotation_matrix
rotoinversion_matrix
row
rows
rowvector
rpow