Structure integrationTheory

signature integrationTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FINE : thm
    val absolutely_integrable_on : thm
    val content : thm
    val division_of : thm
    val division_points : thm
    val equiintegrable_on : thm
    val gauge_def : thm
    val has_bounded_setvariation_on : thm
    val has_bounded_variation_on : thm
    val has_integral_compact_interval : thm
    val has_integral_def : thm
    val indicator : thm
    val integrable_on : thm
    val integral : thm
    val interval_lowerbound : thm
    val interval_upperbound : thm
    val negligible : thm
    val operative : thm
    val set_variation : thm
    val tagged_division_of : thm
    val tagged_partial_division_of : thm
    val vector_variation : thm
  
  (*  Theorems  *)
    val ABSOLUTELY_INTEGRABLE_0 : thm
    val ABSOLUTELY_INTEGRABLE_ABS : thm
    val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_BOUND : thm
    val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_LBOUND : thm
    val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND : thm
    val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_LBOUND : thm
    val ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_UBOUND : thm
    val ABSOLUTELY_INTEGRABLE_ABS_EQ : thm
    val ABSOLUTELY_INTEGRABLE_ADD : thm
    val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION : thm
    val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ : thm
    val ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_UNIV_EQ : thm
    val ABSOLUTELY_INTEGRABLE_CMUL : thm
    val ABSOLUTELY_INTEGRABLE_COMPONENTWISE : thm
    val ABSOLUTELY_INTEGRABLE_CONST : thm
    val ABSOLUTELY_INTEGRABLE_CONTINUOUS : thm
    val ABSOLUTELY_INTEGRABLE_EQ : thm
    val ABSOLUTELY_INTEGRABLE_IMP_ABS_INTEGRABLE : thm
    val ABSOLUTELY_INTEGRABLE_IMP_INTEGRABLE : thm
    val ABSOLUTELY_INTEGRABLE_INF : thm
    val ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND : thm
    val ABSOLUTELY_INTEGRABLE_LE : thm
    val ABSOLUTELY_INTEGRABLE_LINEAR : thm
    val ABSOLUTELY_INTEGRABLE_MAX : thm
    val ABSOLUTELY_INTEGRABLE_MIN : thm
    val ABSOLUTELY_INTEGRABLE_NEG : thm
    val ABSOLUTELY_INTEGRABLE_ON_NULL : thm
    val ABSOLUTELY_INTEGRABLE_ON_SUBINTERVAL : thm
    val ABSOLUTELY_INTEGRABLE_RESTRICT_INTER : thm
    val ABSOLUTELY_INTEGRABLE_RESTRICT_UNIV : thm
    val ABSOLUTELY_INTEGRABLE_SET_VARIATION : thm
    val ABSOLUTELY_INTEGRABLE_SPIKE : thm
    val ABSOLUTELY_INTEGRABLE_SUB : thm
    val ABSOLUTELY_INTEGRABLE_SUM : thm
    val ABSOLUTELY_INTEGRABLE_SUP : thm
    val ABS_LE_L1 : thm
    val ABS_TRIANGLE_LE : thm
    val ADDITIVE_CONTENT_DIVISION : thm
    val ADDITIVE_CONTENT_TAGGED_DIVISION : thm
    val ADDITIVE_TAGGED_DIVISION_1 : thm
    val ANTIDERIVATIVE_CONTINUOUS : thm
    val ANTIDERIVATIVE_INTEGRAL_CONTINUOUS : thm
    val APPROXIMABLE_ON_DIVISION : thm
    val BEPPO_LEVI_DECREASING : thm
    val BEPPO_LEVI_INCREASING : thm
    val BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING : thm
    val BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE : thm
    val BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING : thm
    val BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE : thm
    val BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION : thm
    val BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE : thm
    val BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL : thm
    val CONTENT_0_SUBSET : thm
    val CONTENT_0_SUBSET_GEN : thm
    val CONTENT_CLOSED_INTERVAL : thm
    val CONTENT_CLOSED_INTERVAL_CASES : thm
    val CONTENT_DOUBLESPLIT : thm
    val CONTENT_EMPTY : thm
    val CONTENT_EQ_0 : thm
    val CONTENT_EQ_0_1 : thm
    val CONTENT_EQ_0_GEN : thm
    val CONTENT_EQ_0_INTERIOR : thm
    val CONTENT_IMAGE_AFFINITY_INTERVAL : thm
    val CONTENT_IMAGE_STRETCH_INTERVAL : thm
    val CONTENT_LT_NZ : thm
    val CONTENT_POS_LE : thm
    val CONTENT_POS_LT : thm
    val CONTENT_POS_LT_EQ : thm
    val CONTENT_SPLIT : thm
    val CONTENT_SUBSET : thm
    val CONTENT_UNIT : thm
    val CONTINUOUS_ON_VECTOR_VARIATION : thm
    val CONVEX_CONTAINS_SEGMENT : thm
    val DECREASING_BOUNDED_VARIATION : thm
    val DECREASING_BOUNDED_VARIATION_GEN : thm
    val DECREASING_LEFT_LIMIT : thm
    val DECREASING_RIGHT_LIMIT : thm
    val DECREASING_VECTOR_VARIATION : thm
    val DIVISION_1_SORT : thm
    val DIVISION_COMMON_POINT_BOUND : thm
    val DIVISION_CONTAINS : thm
    val DIVISION_DISJOINT_UNION : thm
    val DIVISION_DOUBLESPLIT : thm
    val DIVISION_INTER : thm
    val DIVISION_INTER_1 : thm
    val DIVISION_OF : thm
    val DIVISION_OF_AFFINITY : thm
    val DIVISION_OF_BIGUNION : thm
    val DIVISION_OF_CLOSED : thm
    val DIVISION_OF_CONTENT_0 : thm
    val DIVISION_OF_FINITE : thm
    val DIVISION_OF_NONTRIVIAL : thm
    val DIVISION_OF_REFLECT : thm
    val DIVISION_OF_SELF : thm
    val DIVISION_OF_SING : thm
    val DIVISION_OF_SUBSET : thm
    val DIVISION_OF_TAGGED_DIVISION : thm
    val DIVISION_OF_TRANSLATION : thm
    val DIVISION_OF_TRIVIAL : thm
    val DIVISION_OF_UNION_SELF : thm
    val DIVISION_POINTS_FINITE : thm
    val DIVISION_POINTS_PSUBSET : thm
    val DIVISION_POINTS_SUBSET : thm
    val DIVISION_SPLIT : thm
    val DIVISION_SPLIT_LEFT_INJ : thm
    val DIVISION_SPLIT_LEFT_RIGHT_INJ : thm
    val DIVISION_SPLIT_RIGHT_INJ : thm
    val DIVISION_UNION_INTERVALS_EXISTS : thm
    val DOMINATED_CONVERGENCE : thm
    val DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE : thm
    val DOMINATED_CONVERGENCE_AE : thm
    val DOMINATED_CONVERGENCE_INTEGRABLE : thm
    val DROP_INDICATOR : thm
    val DROP_INDICATOR_ABS_LE_1 : thm
    val DROP_INDICATOR_LE_1 : thm
    val DROP_INDICATOR_POS_LE : thm
    val DSUM_BOUND : thm
    val ELEMENTARY_BIGINTER : thm
    val ELEMENTARY_BIGUNION_INTERVALS : thm
    val ELEMENTARY_BOUNDED : thm
    val ELEMENTARY_COMPACT : thm
    val ELEMENTARY_EMPTY : thm
    val ELEMENTARY_INTER : thm
    val ELEMENTARY_INTERVAL : thm
    val ELEMENTARY_SUBSET_INTERVAL : thm
    val ELEMENTARY_UNION : thm
    val ELEMENTARY_UNION_INTERVAL : thm
    val ELEMENTARY_UNION_INTERVAL_STRONG : thm
    val EMPTY_DIVISION_OF : thm
    val EQUIINTEGRABLE_ADD : thm
    val EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS : thm
    val EQUIINTEGRABLE_CMUL : thm
    val EQUIINTEGRABLE_DIVISION : thm
    val EQUIINTEGRABLE_EQ : thm
    val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE : thm
    val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT : thm
    val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE : thm
    val EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT : thm
    val EQUIINTEGRABLE_LIMIT : thm
    val EQUIINTEGRABLE_NEG : thm
    val EQUIINTEGRABLE_ON_NULL : thm
    val EQUIINTEGRABLE_ON_SING : thm
    val EQUIINTEGRABLE_ON_SPLIT : thm
    val EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS : thm
    val EQUIINTEGRABLE_REFLECT : thm
    val EQUIINTEGRABLE_SUB : thm
    val EQUIINTEGRABLE_SUBSET : thm
    val EQUIINTEGRABLE_SUM : thm
    val EQUIINTEGRABLE_UNIFORM_LIMIT : thm
    val EQUIINTEGRABLE_UNION : thm
    val FATOU : thm
    val FINE_BIGINTER : thm
    val FINE_BIGUNION : thm
    val FINE_DIVISION_EXISTS : thm
    val FINE_INTER : thm
    val FINE_SUBSET : thm
    val FINE_UNION : thm
    val FINITE_POWERSET : thm
    val FLOOR_POS : thm
    val FORALL_IN_DIVISION : thm
    val FORALL_IN_DIVISION_NONEMPTY : thm
    val FUNDAMENTAL_THEOREM_OF_CALCULUS : thm
    val FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR : thm
    val FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG : thm
    val FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG : thm
    val GAUGE_BALL : thm
    val GAUGE_BALL_DEPENDENT : thm
    val GAUGE_BIGINTER : thm
    val GAUGE_EXISTENCE_LEMMA : thm
    val GAUGE_INTER : thm
    val GAUGE_MODIFY : thm
    val GAUGE_TRIVIAL : thm
    val HAS_BOUNDED_SETVARIATION_COMPARISON : thm
    val HAS_BOUNDED_SETVARIATION_ON : thm
    val HAS_BOUNDED_SETVARIATION_ON_0 : thm
    val HAS_BOUNDED_SETVARIATION_ON_ABS : thm
    val HAS_BOUNDED_SETVARIATION_ON_ADD : thm
    val HAS_BOUNDED_SETVARIATION_ON_CMUL : thm
    val HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE : thm
    val HAS_BOUNDED_SETVARIATION_ON_COMPOSE_LINEAR : thm
    val HAS_BOUNDED_SETVARIATION_ON_DIVISION : thm
    val HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY : thm
    val HAS_BOUNDED_SETVARIATION_ON_EQ : thm
    val HAS_BOUNDED_SETVARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS : thm
    val HAS_BOUNDED_SETVARIATION_ON_INTERVAL : thm
    val HAS_BOUNDED_SETVARIATION_ON_NEG : thm
    val HAS_BOUNDED_SETVARIATION_ON_NULL : thm
    val HAS_BOUNDED_SETVARIATION_ON_SUB : thm
    val HAS_BOUNDED_SETVARIATION_ON_SUBSET : thm
    val HAS_BOUNDED_SETVARIATION_ON_SUM : thm
    val HAS_BOUNDED_SETVARIATION_ON_SUM_AND_SET_VARIATION_SUM_LE : thm
    val HAS_BOUNDED_SETVARIATION_ON_UNIV : thm
    val HAS_BOUNDED_SETVARIATION_REFLECT2_EQ : thm
    val HAS_BOUNDED_SETVARIATION_REFLECT2_EQ_AND_SET_VARIATION_REFLECT2 : thm
    val HAS_BOUNDED_SETVARIATION_TRANSLATION : thm
    val HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ : thm
    val HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ_AND_SET_VARIATION_TRANSLATION2 : thm
    val HAS_BOUNDED_SETVARIATION_WORKS : thm
    val HAS_BOUNDED_SETVARIATION_WORKS_ON_ELEMENTARY : thm
    val HAS_BOUNDED_SETVARIATION_WORKS_ON_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_AFFINITY2_EQ : thm
    val HAS_BOUNDED_VARIATION_AFFINITY2_EQ_AND_VECTOR_VARIATION_AFFINITY2 : thm
    val HAS_BOUNDED_VARIATION_AFFINITY_EQ : thm
    val HAS_BOUNDED_VARIATION_AFFINITY_EQ_AND_VECTOR_VARIATION_AFFINITY : thm
    val HAS_BOUNDED_VARIATION_COMPARISON : thm
    val HAS_BOUNDED_VARIATION_COMPOSE_DECREASING : thm
    val HAS_BOUNDED_VARIATION_COMPOSE_INCREASING : thm
    val HAS_BOUNDED_VARIATION_DARBOUX : thm
    val HAS_BOUNDED_VARIATION_DARBOUX_STRICT : thm
    val HAS_BOUNDED_VARIATION_DARBOUX_STRONG : thm
    val HAS_BOUNDED_VARIATION_NONTRIVIAL : thm
    val HAS_BOUNDED_VARIATION_ON_ABS : thm
    val HAS_BOUNDED_VARIATION_ON_ADD : thm
    val HAS_BOUNDED_VARIATION_ON_CLOSURE : thm
    val HAS_BOUNDED_VARIATION_ON_CMUL : thm
    val HAS_BOUNDED_VARIATION_ON_COMBINE : thm
    val HAS_BOUNDED_VARIATION_ON_COMBINE_GEN : thm
    val HAS_BOUNDED_VARIATION_ON_COMPONENTWISE : thm
    val HAS_BOUNDED_VARIATION_ON_COMPOSE_LINEAR : thm
    val HAS_BOUNDED_VARIATION_ON_CONST : thm
    val HAS_BOUNDED_VARIATION_ON_DIVISION : thm
    val HAS_BOUNDED_VARIATION_ON_EMPTY : thm
    val HAS_BOUNDED_VARIATION_ON_EQ : thm
    val HAS_BOUNDED_VARIATION_ON_ID : thm
    val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED : thm
    val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS : thm
    val HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_LEFT : thm
    val HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_RIGHT : thm
    val HAS_BOUNDED_VARIATION_ON_MAX : thm
    val HAS_BOUNDED_VARIATION_ON_MIN : thm
    val HAS_BOUNDED_VARIATION_ON_MUL : thm
    val HAS_BOUNDED_VARIATION_ON_NEG : thm
    val HAS_BOUNDED_VARIATION_ON_NULL : thm
    val HAS_BOUNDED_VARIATION_ON_REFLECT : thm
    val HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_ON_SING : thm
    val HAS_BOUNDED_VARIATION_ON_SUB : thm
    val HAS_BOUNDED_VARIATION_ON_SUBSET : thm
    val HAS_BOUNDED_VARIATION_ON_SUM : thm
    val HAS_BOUNDED_VARIATION_ON_SUM_AND_SUM_LE : thm
    val HAS_BOUNDED_VARIATION_REFLECT2_EQ : thm
    val HAS_BOUNDED_VARIATION_REFLECT2_EQ_AND_VECTOR_VARIATION_REFLECT2 : thm
    val HAS_BOUNDED_VARIATION_REFLECT_EQ : thm
    val HAS_BOUNDED_VARIATION_REFLECT_EQ_AND_VECTOR_VARIATION_REFLECT : thm
    val HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL_AND_VECTOR_VARIATION_REFLECT_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_SUM_LE : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION2_EQ : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION2_EQ_AND_VECTOR_VARIATION_TRANSLATION2 : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION_EQ : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_AND_VECTOR_VARIATION_TRANSLATION : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL : thm
    val HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL_AND_VECTOR_VARIATION_TRANSLATION_INTERVAL : thm
    val HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT : thm
    val HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT : thm
    val HAS_DERIVATIVE_ZERO_UNIQUE_STRONG_INTERVAL : thm
    val HAS_INTEGRAL : thm
    val HAS_INTEGRAL_0 : thm
    val HAS_INTEGRAL_0_EQ : thm
    val HAS_INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT : thm
    val HAS_INTEGRAL_ADD : thm
    val HAS_INTEGRAL_AFFINITY : thm
    val HAS_INTEGRAL_ALT : thm
    val HAS_INTEGRAL_BIGUNION : thm
    val HAS_INTEGRAL_BOUND : thm
    val HAS_INTEGRAL_CLOSURE : thm
    val HAS_INTEGRAL_CMUL : thm
    val HAS_INTEGRAL_COMBINE : thm
    val HAS_INTEGRAL_COMBINE_DIVISION : thm
    val HAS_INTEGRAL_COMBINE_DIVISION_TOPDOWN : thm
    val HAS_INTEGRAL_COMBINE_TAGGED_DIVISION : thm
    val HAS_INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN : thm
    val HAS_INTEGRAL_COMPONENTWISE : thm
    val HAS_INTEGRAL_COMPONENT_LBOUND : thm
    val HAS_INTEGRAL_COMPONENT_LE : thm
    val HAS_INTEGRAL_COMPONENT_LE_AE : thm
    val HAS_INTEGRAL_COMPONENT_NEG : thm
    val HAS_INTEGRAL_COMPONENT_POS : thm
    val HAS_INTEGRAL_COMPONENT_UBOUND : thm
    val HAS_INTEGRAL_CONST : thm
    val HAS_INTEGRAL_DIFF : thm
    val HAS_INTEGRAL_DROP_LE : thm
    val HAS_INTEGRAL_DROP_NEG : thm
    val HAS_INTEGRAL_DROP_POS : thm
    val HAS_INTEGRAL_DROP_POS_AE : thm
    val HAS_INTEGRAL_EMPTY : thm
    val HAS_INTEGRAL_EMPTY_EQ : thm
    val HAS_INTEGRAL_EQ : thm
    val HAS_INTEGRAL_EQ_EQ : thm
    val HAS_INTEGRAL_FACTOR_CONTENT : thm
    val HAS_INTEGRAL_INTEGRABLE : thm
    val HAS_INTEGRAL_INTEGRABLE_INTEGRAL : thm
    val HAS_INTEGRAL_INTEGRAL : thm
    val HAS_INTEGRAL_INTERIOR : thm
    val HAS_INTEGRAL_IS_0 : thm
    val HAS_INTEGRAL_LE_AE : thm
    val HAS_INTEGRAL_LIM_AT_POSINFINITY : thm
    val HAS_INTEGRAL_LIM_SEQUENTIALLY : thm
    val HAS_INTEGRAL_LINEAR : thm
    val HAS_INTEGRAL_NEG : thm
    val HAS_INTEGRAL_NEGLIGIBLE : thm
    val HAS_INTEGRAL_NEGLIGIBLE_EQ : thm
    val HAS_INTEGRAL_NULL : thm
    val HAS_INTEGRAL_NULL_EQ : thm
    val HAS_INTEGRAL_ON_SUPERSET : thm
    val HAS_INTEGRAL_REFL : thm
    val HAS_INTEGRAL_REFLECT : thm
    val HAS_INTEGRAL_REFLECT_GEN : thm
    val HAS_INTEGRAL_REFLECT_LEMMA : thm
    val HAS_INTEGRAL_RESTRICT : thm
    val HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVAL : thm
    val HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVALS_EQ : thm
    val HAS_INTEGRAL_RESTRICT_INTER : thm
    val HAS_INTEGRAL_RESTRICT_OPEN_SUBINTERVAL : thm
    val HAS_INTEGRAL_RESTRICT_UNIV : thm
    val HAS_INTEGRAL_SEPARATE_SIDES : thm
    val HAS_INTEGRAL_SPIKE : thm
    val HAS_INTEGRAL_SPIKE_EQ : thm
    val HAS_INTEGRAL_SPIKE_FINITE : thm
    val HAS_INTEGRAL_SPIKE_FINITE_EQ : thm
    val HAS_INTEGRAL_SPIKE_INTERIOR : thm
    val HAS_INTEGRAL_SPIKE_INTERIOR_EQ : thm
    val HAS_INTEGRAL_SPIKE_SET : thm
    val HAS_INTEGRAL_SPIKE_SET_EQ : thm
    val HAS_INTEGRAL_SPLIT : thm
    val HAS_INTEGRAL_STRADDLE_NULL : thm
    val HAS_INTEGRAL_STRETCH : thm
    val HAS_INTEGRAL_SUB : thm
    val HAS_INTEGRAL_SUBSET_COMPONENT_LE : thm
    val HAS_INTEGRAL_SUBSET_DROP_LE : thm
    val HAS_INTEGRAL_SUM : thm
    val HAS_INTEGRAL_TWIDDLE : thm
    val HAS_INTEGRAL_UNION : thm
    val HAS_INTEGRAL_UNIQUE : thm
    val HENSTOCK_LEMMA : thm
    val HENSTOCK_LEMMA_PART1 : thm
    val HENSTOCK_LEMMA_PART2 : thm
    val INCREASING_BOUNDED_VARIATION : thm
    val INCREASING_BOUNDED_VARIATION_GEN : thm
    val INCREASING_LEFT_LIMIT : thm
    val INCREASING_RIGHT_LIMIT : thm
    val INCREASING_VECTOR_VARIATION : thm
    val INDEFINITE_INTEGRAL_CONTINUOUS : thm
    val INDEFINITE_INTEGRAL_CONTINUOUS_LEFT : thm
    val INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT : thm
    val INDICATOR_EMPTY : thm
    val INTEGRABLE_0 : thm
    val INTEGRABLE_ADD : thm
    val INTEGRABLE_AFFINITY : thm
    val INTEGRABLE_ALT : thm
    val INTEGRABLE_ALT_SUBSET : thm
    val INTEGRABLE_BOUNDED_VARIATION : thm
    val INTEGRABLE_BOUNDED_VARIATION_BILINEAR_LMUL : thm
    val INTEGRABLE_BOUNDED_VARIATION_BILINEAR_RMUL : thm
    val INTEGRABLE_BOUNDED_VARIATION_PRODUCT : thm
    val INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT : thm
    val INTEGRABLE_BY_PARTS : thm
    val INTEGRABLE_BY_PARTS_EQ : thm
    val INTEGRABLE_CASES : thm
    val INTEGRABLE_CAUCHY : thm
    val INTEGRABLE_CMUL : thm
    val INTEGRABLE_CMUL_EQ : thm
    val INTEGRABLE_COMBINE : thm
    val INTEGRABLE_COMBINE_DIVISION : thm
    val INTEGRABLE_COMPONENTWISE : thm
    val INTEGRABLE_CONST : thm
    val INTEGRABLE_CONTINUOUS : thm
    val INTEGRABLE_DECREASING : thm
    val INTEGRABLE_DECREASING_PRODUCT : thm
    val INTEGRABLE_DECREASING_PRODUCT_UNIV : thm
    val INTEGRABLE_EQ : thm
    val INTEGRABLE_INCREASING : thm
    val INTEGRABLE_INCREASING_PRODUCT : thm
    val INTEGRABLE_INCREASING_PRODUCT_UNIV : thm
    val INTEGRABLE_INTEGRAL : thm
    val INTEGRABLE_LINEAR : thm
    val INTEGRABLE_MIN_CONST : thm
    val INTEGRABLE_NEG : thm
    val INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND : thm
    val INTEGRABLE_ON_EMPTY : thm
    val INTEGRABLE_ON_LITTLE_SUBINTERVALS : thm
    val INTEGRABLE_ON_NULL : thm
    val INTEGRABLE_ON_REFL : thm
    val INTEGRABLE_ON_SUBDIVISION : thm
    val INTEGRABLE_ON_SUBINTERVAL : thm
    val INTEGRABLE_ON_SUPERSET : thm
    val INTEGRABLE_REFLECT : thm
    val INTEGRABLE_REFLECT_GEN : thm
    val INTEGRABLE_RESTRICT : thm
    val INTEGRABLE_RESTRICT_INTER : thm
    val INTEGRABLE_RESTRICT_UNIV : thm
    val INTEGRABLE_SPIKE : thm
    val INTEGRABLE_SPIKE_EQ : thm
    val INTEGRABLE_SPIKE_FINITE : thm
    val INTEGRABLE_SPIKE_INTERIOR : thm
    val INTEGRABLE_SPIKE_SET : thm
    val INTEGRABLE_SPIKE_SET_EQ : thm
    val INTEGRABLE_SPLIT : thm
    val INTEGRABLE_STRADDLE : thm
    val INTEGRABLE_STRADDLE_INTERVAL : thm
    val INTEGRABLE_STRETCH : thm
    val INTEGRABLE_SUB : thm
    val INTEGRABLE_SUBINTERVAL : thm
    val INTEGRABLE_SUM : thm
    val INTEGRABLE_UNIFORM_LIMIT : thm
    val INTEGRAL_0 : thm
    val INTEGRAL_ABS_BOUND_INTEGRAL : thm
    val INTEGRAL_ABS_BOUND_INTEGRAL_AE : thm
    val INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT : thm
    val INTEGRAL_ADD : thm
    val INTEGRAL_CMUL : thm
    val INTEGRAL_COMBINE : thm
    val INTEGRAL_COMBINE_DIVISION_BOTTOMUP : thm
    val INTEGRAL_COMBINE_DIVISION_TOPDOWN : thm
    val INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP : thm
    val INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN : thm
    val INTEGRAL_COMPONENT : thm
    val INTEGRAL_COMPONENT_LBOUND : thm
    val INTEGRAL_COMPONENT_LE : thm
    val INTEGRAL_COMPONENT_LE_AE : thm
    val INTEGRAL_COMPONENT_POS : thm
    val INTEGRAL_COMPONENT_UBOUND : thm
    val INTEGRAL_CONST : thm
    val INTEGRAL_DIFF : thm
    val INTEGRAL_DROP_LE : thm
    val INTEGRAL_DROP_POS : thm
    val INTEGRAL_DROP_POS_AE : thm
    val INTEGRAL_EMPTY : thm
    val INTEGRAL_EQ : thm
    val INTEGRAL_EQ_0 : thm
    val INTEGRAL_EQ_HAS_INTEGRAL : thm
    val INTEGRAL_HAS_VECTOR_DERIVATIVE : thm
    val INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE : thm
    val INTEGRAL_LE_AE : thm
    val INTEGRAL_LINEAR : thm
    val INTEGRAL_NEG : thm
    val INTEGRAL_NULL : thm
    val INTEGRAL_REFL : thm
    val INTEGRAL_REFLECT : thm
    val INTEGRAL_REFLECT_GEN : thm
    val INTEGRAL_RESTRICT : thm
    val INTEGRAL_RESTRICT_INTER : thm
    val INTEGRAL_RESTRICT_UNIV : thm
    val INTEGRAL_SPIKE : thm
    val INTEGRAL_SPIKE_SET : thm
    val INTEGRAL_SPLIT : thm
    val INTEGRAL_SPLIT_SIGNED : thm
    val INTEGRAL_SUB : thm
    val INTEGRAL_SUBSET_COMPONENT_LE : thm
    val INTEGRAL_SUBSET_DROP_LE : thm
    val INTEGRAL_SUM : thm
    val INTEGRAL_UNION : thm
    val INTEGRAL_UNIQUE : thm
    val INTEGRATION_BY_PARTS : thm
    val INTEGRATION_BY_PARTS_SIMPLE : thm
    val INTERIOR_SUBSET_UNION_INTERVALS : thm
    val INTERVAL_BISECTION : thm
    val INTERVAL_BISECTION_STEP : thm
    val INTERVAL_BOUNDS_EMPTY : thm
    val INTERVAL_BOUNDS_NULL : thm
    val INTERVAL_DOUBLESPLIT : thm
    val INTERVAL_IMAGE_AFFINITY_INTERVAL : thm
    val INTERVAL_LOWERBOUND : thm
    val INTERVAL_LOWERBOUND_NONEMPTY : thm
    val INTERVAL_SPLIT : thm
    val INTERVAL_SUBDIVISION : thm
    val INTERVAL_UPPERBOUND : thm
    val INTERVAL_UPPERBOUND_NONEMPTY : thm
    val INTER_INTERIOR_BIGUNION_INTERVALS : thm
    val ITERATE_AND : thm
    val ITERATE_NONZERO_IMAGE_LEMMA : thm
    val ITERATE_SOME : thm
    val MONOIDAL_AND : thm
    val MONOIDAL_LIFTED : thm
    val MONOTONE_CONVERGENCE_DECREASING : thm
    val MONOTONE_CONVERGENCE_DECREASING_AE : thm
    val MONOTONE_CONVERGENCE_INCREASING : thm
    val MONOTONE_CONVERGENCE_INCREASING_AE : thm
    val MONOTONE_CONVERGENCE_INTERVAL : thm
    val NEGLIGIBLE : thm
    val NEGLIGIBLE_BIGUNION : thm
    val NEGLIGIBLE_BOUNDED_SUBSETS : thm
    val NEGLIGIBLE_COUNTABLE : thm
    val NEGLIGIBLE_COUNTABLE_BIGUNION : thm
    val NEGLIGIBLE_DIFF : thm
    val NEGLIGIBLE_EMPTY : thm
    val NEGLIGIBLE_FINITE : thm
    val NEGLIGIBLE_FRONTIER_INTERVAL : thm
    val NEGLIGIBLE_INSERT : thm
    val NEGLIGIBLE_INTER : thm
    val NEGLIGIBLE_ON_COUNTABLE_INTERVALS : thm
    val NEGLIGIBLE_ON_INTERVALS : thm
    val NEGLIGIBLE_ON_UNIV : thm
    val NEGLIGIBLE_SING : thm
    val NEGLIGIBLE_STANDARD_HYPERPLANE : thm
    val NEGLIGIBLE_SUBSET : thm
    val NEGLIGIBLE_UNION : thm
    val NEGLIGIBLE_UNION_EQ : thm
    val NEUTRAL_AND : thm
    val NEUTRAL_LIFTED : thm
    val NONNEGATIVE_ABSOLUTELY_INTEGRABLE : thm
    val NONNEGATIVE_ABSOLUTELY_INTEGRABLE_AE : thm
    val OPEN_INTERVAL_LOWERBOUND : thm
    val OPEN_INTERVAL_UPPERBOUND : thm
    val OPERATIVE_1_LE : thm
    val OPERATIVE_1_LT : thm
    val OPERATIVE_APPROXIMABLE : thm
    val OPERATIVE_CONTENT : thm
    val OPERATIVE_DIVISION : thm
    val OPERATIVE_DIVISION_AND : thm
    val OPERATIVE_EMPTY : thm
    val OPERATIVE_FUNCTION_ENDPOINT_DIFF : thm
    val OPERATIVE_INTEGRABLE : thm
    val OPERATIVE_INTEGRAL : thm
    val OPERATIVE_LIFTED_SETVARIATION : thm
    val OPERATIVE_LIFTED_VECTOR_VARIATION : thm
    val OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF : thm
    val OPERATIVE_TAGGED_DIVISION : thm
    val OPERATIVE_TRIVIAL : thm
    val PARTIAL_DIVISION_EXTEND : thm
    val PARTIAL_DIVISION_EXTEND_1 : thm
    val PARTIAL_DIVISION_EXTEND_INTERVAL : thm
    val PARTIAL_DIVISION_OF_TAGGED_DIVISION : thm
    val PROPERTY_EMPTY_INTERVAL : thm
    val REAL_MUL_POS_LT : thm
    val REAL_SUP_LE_FINITE : thm
    val RSUM_BOUND : thm
    val RSUM_COMPONENT_LE : thm
    val RSUM_DIFF_BOUND : thm
    val SECOND_MEAN_VALUE_THEOREM : thm
    val SECOND_MEAN_VALUE_THEOREM_BONNET : thm
    val SECOND_MEAN_VALUE_THEOREM_BONNET_FULL : thm
    val SECOND_MEAN_VALUE_THEOREM_FULL : thm
    val SECOND_MEAN_VALUE_THEOREM_GEN : thm
    val SECOND_MEAN_VALUE_THEOREM_GEN_FULL : thm
    val SETVARIATION_EQUAL_LEMMA : thm
    val SET_VARIATION : thm
    val SET_VARIATION_0 : thm
    val SET_VARIATION_COMPARISON : thm
    val SET_VARIATION_ELEMENTARY_LEMMA : thm
    val SET_VARIATION_EQ : thm
    val SET_VARIATION_GE_FUNCTION : thm
    val SET_VARIATION_LBOUND : thm
    val SET_VARIATION_LBOUND_ON_INTERVAL : thm
    val SET_VARIATION_MONOTONE : thm
    val SET_VARIATION_ON_DIVISION : thm
    val SET_VARIATION_ON_ELEMENTARY : thm
    val SET_VARIATION_ON_INTERVAL : thm
    val SET_VARIATION_ON_NULL : thm
    val SET_VARIATION_POS_LE : thm
    val SET_VARIATION_REFLECT2 : thm
    val SET_VARIATION_SUM_LE : thm
    val SET_VARIATION_TRANSLATION2 : thm
    val SET_VARIATION_TRIANGLE : thm
    val SET_VARIATION_UBOUND : thm
    val SET_VARIATION_UBOUND_ON_INTERVAL : thm
    val SET_VARIATION_WORKS_ON_INTERVAL : thm
    val SUBADDITIVE_CONTENT_DIVISION : thm
    val SUM_ABS_ALLSUBSETS_BOUND : thm
    val SUM_CONTENT_AREA_OVER_THIN_DIVISION : thm
    val SUM_CONTENT_NULL : thm
    val SUM_NONZERO_IMAGE_LEMMA : thm
    val SUM_OVER_TAGGED_DIVISION_LEMMA : thm
    val SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA : thm
    val SUP_FINITE : thm
    val SUP_FINITE_LEMMA : thm
    val TAGGED_DIVISION_BIGUNION : thm
    val TAGGED_DIVISION_BIGUNION_EXISTS : thm
    val TAGGED_DIVISION_FINER : thm
    val TAGGED_DIVISION_OF : thm
    val TAGGED_DIVISION_OF_ALT : thm
    val TAGGED_DIVISION_OF_ANOTHER : thm
    val TAGGED_DIVISION_OF_EMPTY : thm
    val TAGGED_DIVISION_OF_FINITE : thm
    val TAGGED_DIVISION_OF_NONTRIVIAL : thm
    val TAGGED_DIVISION_OF_SELF : thm
    val TAGGED_DIVISION_OF_TRIVIAL : thm
    val TAGGED_DIVISION_OF_UNION_SELF : thm
    val TAGGED_DIVISION_SPLIT_LEFT_INJ : thm
    val TAGGED_DIVISION_SPLIT_RIGHT_INJ : thm
    val TAGGED_DIVISION_UNION : thm
    val TAGGED_DIVISION_UNION_IMAGE_SND : thm
    val TAGGED_DIVISION_UNION_INTERVAL : thm
    val TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND : thm
    val TAGGED_PARTIAL_DIVISION_COMMON_TAGS : thm
    val TAGGED_PARTIAL_DIVISION_OF_SUBSET : thm
    val TAGGED_PARTIAL_DIVISION_OF_TRIVIAL : thm
    val TAGGED_PARTIAL_DIVISION_OF_UNION_SELF : thm
    val TAGGED_PARTIAL_DIVISION_SUBSET : thm
    val TAG_IN_INTERVAL : thm
    val VARIATION_EQUAL_LEMMA : thm
    val VECTOR_VARIATION_ABS : thm
    val VECTOR_VARIATION_AFFINITY : thm
    val VECTOR_VARIATION_AFFINITY2 : thm
    val VECTOR_VARIATION_COMBINE : thm
    val VECTOR_VARIATION_COMPARISON : thm
    val VECTOR_VARIATION_CONST : thm
    val VECTOR_VARIATION_CONST_EQ : thm
    val VECTOR_VARIATION_CONTINUOUS : thm
    val VECTOR_VARIATION_CONTINUOUS_LEFT : thm
    val VECTOR_VARIATION_CONTINUOUS_RIGHT : thm
    val VECTOR_VARIATION_EQ : thm
    val VECTOR_VARIATION_GE_ABS_FUNCTION : thm
    val VECTOR_VARIATION_GE_FUNCTION : thm
    val VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE : thm
    val VECTOR_VARIATION_MONOTONE : thm
    val VECTOR_VARIATION_NEG : thm
    val VECTOR_VARIATION_ON_DIVISION : thm
    val VECTOR_VARIATION_ON_NULL : thm
    val VECTOR_VARIATION_POS_LE : thm
    val VECTOR_VARIATION_REFLECT : thm
    val VECTOR_VARIATION_REFLECT2 : thm
    val VECTOR_VARIATION_REFLECT_INTERVAL : thm
    val VECTOR_VARIATION_TRANSLATION : thm
    val VECTOR_VARIATION_TRANSLATION2 : thm
    val VECTOR_VARIATION_TRANSLATION_INTERVAL : thm
    val VECTOR_VARIATION_TRIANGLE : thm
    val has_integral : thm
    val has_integral_alt : thm
    val lifted_def : thm
    val lifted_ind : thm
  
  val integration_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [derivative] Parent theory of "integration"
   
   [FINE]  Definition
      
      ⊢ ∀d s. d FINE s ⇔ ∀x k. (x,k) ∈ s ⇒ k ⊆ d x
   
   [absolutely_integrable_on]  Definition
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇔
          f integrable_on s ∧ (λx. abs (f x)) integrable_on s
   
   [content]  Definition
      
      ⊢ ∀s. content s =
            if s = ∅ then 0
            else interval_upperbound s − interval_lowerbound s
   
   [division_of]  Definition
      
      ⊢ ∀s i.
          s division_of i ⇔
          FINITE s ∧
          (∀k. k ∈ s ⇒ k ⊆ i ∧ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
          (∀k1 k2.
             k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ interior k1 ∩ interior k2 = ∅) ∧
          BIGUNION s = i
   
   [division_points]  Definition
      
      ⊢ ∀k d.
          division_points k d =
          {(j,x) |
           1 ≤ j ∧ j ≤ 1 ∧ interval_lowerbound k < x ∧
           x < interval_upperbound k ∧
           ∃i. i ∈ d ∧
               (interval_lowerbound i = x ∨ interval_upperbound i = x)}
   
   [equiintegrable_on]  Definition
      
      ⊢ ∀fs i.
          fs equiintegrable_on i ⇔
          (∀f. f ∈ fs ⇒ f integrable_on i) ∧
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀f p.
                    f ∈ fs ∧ p tagged_division_of i ∧ d FINE p ⇒
                    abs (sum p (λ(x,k). content k * f x) − integral i f) <
                    e
   
   [gauge_def]  Definition
      
      ⊢ ∀d. gauge d ⇔ ∀x. x ∈ d x ∧ open (d x)
   
   [has_bounded_setvariation_on]  Definition
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ⇔
          ∃B. ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B
   
   [has_bounded_variation_on]  Definition
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇔
          (λk. f (interval_upperbound k) − f (interval_lowerbound k)) has_bounded_setvariation_on
          s
   
   [has_integral_compact_interval]  Definition
      
      ⊢ ∀f y i.
          (f has_integral_compact_interval y) i ⇔
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀p. p tagged_division_of i ∧ d FINE p ⇒
                      abs (sum p (λ(x,k). content k * f x) − y) < e
   
   [has_integral_def]  Definition
      
      ⊢ ∀f y i.
          (f has_integral y) i ⇔
          if ∃a b. i = interval [(a,b)] then
            (f has_integral_compact_interval y) i
          else
            ∀e. 0 < e ⇒
                ∃B. 0 < B ∧
                    ∀a b.
                      ball (0,B) ⊆ interval [(a,b)] ⇒
                      ∃z. ((λx. if x ∈ i then f x else 0) has_integral_compact_interval
                           z) (interval [(a,b)]) ∧ abs (z − y) < e
   
   [indicator]  Definition
      
      ⊢ ∀s. indicator s = (λx. if x ∈ s then 1 else 0)
   
   [integrable_on]  Definition
      
      ⊢ ∀f i. f integrable_on i ⇔ ∃y. (f has_integral y) i
   
   [integral]  Definition
      
      ⊢ ∀i f. integral i f = @y. (f has_integral y) i
   
   [interval_lowerbound]  Definition
      
      ⊢ ∀s. interval_lowerbound s = if s = ∅ then 0 else inf s
   
   [interval_upperbound]  Definition
      
      ⊢ ∀s. interval_upperbound s = if s = ∅ then 0 else sup s
   
   [negligible]  Definition
      
      ⊢ ∀s. negligible s ⇔
            ∀a b. (indicator s has_integral 0) (interval [(a,b)])
   
   [operative]  Definition
      
      ⊢ ∀op f.
          operative op f ⇔
          (∀a b.
             content (interval [(a,b)]) = 0 ⇒
             f (interval [(a,b)]) = neutral op) ∧
          ∀a b c.
            f (interval [(a,b)]) =
            op (f (interval [(a,b)] ∩ {x | x ≤ c}))
              (f (interval [(a,b)] ∩ {x | x ≥ c}))
   
   [set_variation]  Definition
      
      ⊢ ∀s f.
          set_variation s f =
          sup {sum d (λk. abs (f k)) | (∃t. d division_of t ∧ t ⊆ s)}
   
   [tagged_division_of]  Definition
      
      ⊢ ∀s i.
          s tagged_division_of i ⇔
          s tagged_partial_division_of i ∧
          BIGUNION {k | (∃x. (x,k) ∈ s)} = i
   
   [tagged_partial_division_of]  Definition
      
      ⊢ ∀s i.
          s tagged_partial_division_of i ⇔
          FINITE s ∧
          (∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
          ∀x1 k1 x2 k2.
            (x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
            interior k1 ∩ interior k2 = ∅
   
   [vector_variation]  Definition
      
      ⊢ ∀s f.
          vector_variation s f =
          set_variation s
            (λk. f (interval_upperbound k) − f (interval_lowerbound k))
   
   [ABSOLUTELY_INTEGRABLE_0]  Theorem
      
      ⊢ ∀s. (λx. 0) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABS]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇒
          (λx. abs (f x)) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_BOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ abs (f x) ≤ abs (g x)) ∧ f integrable_on s ∧
          g absolutely_integrable_on s ⇒
          f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_LBOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
          g integrable_on s ⇒
          g absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_COMPONENT_UBOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x i. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
          g absolutely_integrable_on s ⇒
          f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_LBOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
          g integrable_on s ⇒
          g absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABSOLUTELY_INTEGRABLE_UBOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
          g absolutely_integrable_on s ⇒
          f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ABS_EQ]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇔
          f integrable_on s ∧ (λx. abs (f x)) integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ADD]  Theorem
      
      ⊢ ∀f g s.
          f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
          (λx. f x + g x) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇒
          (λk. integral k f) has_bounded_setvariation_on s
   
   [ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ]  Theorem
      
      ⊢ ∀f a b.
          f absolutely_integrable_on interval [(a,b)] ⇔
          f integrable_on interval [(a,b)] ∧
          (λk. integral k f) has_bounded_setvariation_on interval [(a,b)]
   
   [ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_UNIV_EQ]  Theorem
      
      ⊢ ∀f. f absolutely_integrable_on 𝕌(:real) ⇔
            f integrable_on 𝕌(:real) ∧
            (λk. integral k f) has_bounded_setvariation_on 𝕌(:real)
   
   [ABSOLUTELY_INTEGRABLE_CMUL]  Theorem
      
      ⊢ ∀f s c.
          f absolutely_integrable_on s ⇒
          (λx. c * f x) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_COMPONENTWISE]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇔
          (λx. f x) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_CONST]  Theorem
      
      ⊢ ∀a b c. (λx. c) absolutely_integrable_on interval [(a,b)]
   
   [ABSOLUTELY_INTEGRABLE_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b.
          f continuous_on interval [(a,b)] ⇒
          f absolutely_integrable_on interval [(a,b)]
   
   [ABSOLUTELY_INTEGRABLE_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x = g x) ∧ f absolutely_integrable_on s ⇒
          g absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_IMP_ABS_INTEGRABLE]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇒ (λx. abs (f x)) integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_IMP_INTEGRABLE]  Theorem
      
      ⊢ ∀f s. f absolutely_integrable_on s ⇒ f integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_INF]  Theorem
      
      ⊢ ∀fs s k.
          FINITE k ∧ k ≠ ∅ ∧
          (∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
          (λx. inf (IMAGE (fs x) k)) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_INTEGRABLE_BOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ f integrable_on s ∧
          g integrable_on s ⇒
          f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_LE]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇒
          abs (integral s f) ≤ integral s (λx. abs (f x))
   
   [ABSOLUTELY_INTEGRABLE_LINEAR]  Theorem
      
      ⊢ ∀f h s.
          f absolutely_integrable_on s ∧ linear h ⇒
          h ∘ f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_MAX]  Theorem
      
      ⊢ ∀f g s.
          f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
          (λx. max (f x) (g x)) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_MIN]  Theorem
      
      ⊢ ∀f g s.
          f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
          (λx. min (f x) (g x)) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_NEG]  Theorem
      
      ⊢ ∀f s.
          f absolutely_integrable_on s ⇒
          (λx. -f x) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_ON_NULL]  Theorem
      
      ⊢ ∀f a b.
          content (interval [(a,b)]) = 0 ⇒
          f absolutely_integrable_on interval [(a,b)]
   
   [ABSOLUTELY_INTEGRABLE_ON_SUBINTERVAL]  Theorem
      
      ⊢ ∀f s a b.
          f absolutely_integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
          f absolutely_integrable_on interval [(a,b)]
   
   [ABSOLUTELY_INTEGRABLE_RESTRICT_INTER]  Theorem
      
      ⊢ ∀f s t.
          (λx. if x ∈ s then f x else 0) absolutely_integrable_on t ⇔
          f absolutely_integrable_on s ∩ t
   
   [ABSOLUTELY_INTEGRABLE_RESTRICT_UNIV]  Theorem
      
      ⊢ ∀f s.
          (λx. if x ∈ s then f x else 0) absolutely_integrable_on 𝕌(:real) ⇔
          f absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_SET_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          f absolutely_integrable_on interval [(a,b)] ⇒
          set_variation (interval [(a,b)]) (λk. integral k f) =
          integral (interval [(a,b)]) (λx. abs (f x))
   
   [ABSOLUTELY_INTEGRABLE_SPIKE]  Theorem
      
      ⊢ ∀f g s t.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          f absolutely_integrable_on t ⇒
          g absolutely_integrable_on t
   
   [ABSOLUTELY_INTEGRABLE_SUB]  Theorem
      
      ⊢ ∀f g s.
          f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
          (λx. f x − g x) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_SUM]  Theorem
      
      ⊢ ∀f s t.
          FINITE t ∧ (∀a. a ∈ t ⇒ f a absolutely_integrable_on s) ⇒
          (λx. sum t (λa. f a x)) absolutely_integrable_on s
   
   [ABSOLUTELY_INTEGRABLE_SUP]  Theorem
      
      ⊢ ∀fs s k.
          FINITE k ∧ k ≠ ∅ ∧
          (∀i. i ∈ k ⇒ (λx. fs x i) absolutely_integrable_on s) ⇒
          (λx. sup (IMAGE (fs x) k)) absolutely_integrable_on s
   
   [ABS_LE_L1]  Theorem
      
      ⊢ ∀x. abs x ≤ sum (1 .. 1) (λi. abs x)
   
   [ABS_TRIANGLE_LE]  Theorem
      
      ⊢ ∀x y. abs x + abs y ≤ e ⇒ abs (x + y) ≤ e
   
   [ADDITIVE_CONTENT_DIVISION]  Theorem
      
      ⊢ ∀d a b.
          d division_of interval [(a,b)] ⇒
          sum d content = content (interval [(a,b)])
   
   [ADDITIVE_CONTENT_TAGGED_DIVISION]  Theorem
      
      ⊢ ∀d a b.
          d tagged_division_of interval [(a,b)] ⇒
          sum d (λ(x,l). content l) = content (interval [(a,b)])
   
   [ADDITIVE_TAGGED_DIVISION_1]  Theorem
      
      ⊢ ∀f p a b.
          a ≤ b ∧ p tagged_division_of interval [(a,b)] ⇒
          sum p
            (λ(x,k). f (interval_upperbound k) − f (interval_lowerbound k)) =
          f b − f a
   
   [ANTIDERIVATIVE_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b.
          f continuous_on interval [(a,b)] ⇒
          ∃g. ∀x.
            x ∈ interval [(a,b)] ⇒
            (g has_vector_derivative f x) (at x within interval [(a,b)])
   
   [ANTIDERIVATIVE_INTEGRAL_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b.
          f continuous_on interval [(a,b)] ⇒
          ∃g. ∀u v.
            u ∈ interval [(a,b)] ∧ v ∈ interval [(a,b)] ∧ u ≤ v ⇒
            (f has_integral g v − g u) (interval [(u,v)])
   
   [APPROXIMABLE_ON_DIVISION]  Theorem
      
      ⊢ ∀f d a b e.
          0 ≤ e ∧ d division_of interval [(a,b)] ∧
          (∀i. i ∈ d ⇒
               ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i) ⇒
          ∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
              g integrable_on interval [(a,b)]
   
   [BEPPO_LEVI_DECREASING]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            ∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially
   
   [BEPPO_LEVI_INCREASING]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            ∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially
   
   [BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
            g integrable_on s ∧
            ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [BEPPO_LEVI_MONOTONE_CONVERGENCE_DECREASING_AE]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧
          (∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
            g integrable_on s ∧
            ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
            g integrable_on s ∧
            ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [BEPPO_LEVI_MONOTONE_CONVERGENCE_INCREASING_AE]  Theorem
      
      ⊢ ∀f s.
          (∀k. f k integrable_on s) ∧
          (∀k. ∃t. negligible t ∧ ∀x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          ∃g k.
            negligible k ∧
            (∀x. x ∈ s DIFF k ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
            g integrable_on s ∧
            ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [BOUNDED_EQUIINTEGRAL_OVER_THIN_TAGGED_PARTIAL_DIVISION]  Theorem
      
      ⊢ ∀fs f a b e.
          fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
          (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ∧
          0 < e ⇒
          ∃d. gauge d ∧
              ∀c p h.
                c ∈ interval [(a,b)] ∧
                p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ∧
                h ∈ fs ∧ (∀x k. (x,k) ∈ p ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
                sum p (λ(x,k). abs (integral k h)) < e
   
   [BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE]  Theorem
      
      ⊢ ∀f. f integrable_on 𝕌(:real) ∧
            (λk. integral k f) has_bounded_setvariation_on 𝕌(:real) ⇒
            f absolutely_integrable_on 𝕌(:real)
   
   [BOUNDED_SETVARIATION_ABSOLUTELY_INTEGRABLE_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ∧
          (λk. integral k f) has_bounded_setvariation_on interval [(a,b)] ⇒
          f absolutely_integrable_on interval [(a,b)]
   
   [CONTENT_0_SUBSET]  Theorem
      
      ⊢ ∀s a b.
          s ⊆ interval [(a,b)] ∧ content (interval [(a,b)]) = 0 ⇒
          content s = 0
   
   [CONTENT_0_SUBSET_GEN]  Theorem
      
      ⊢ ∀s t. s ⊆ t ∧ bounded t ∧ content t = 0 ⇒ content s = 0
   
   [CONTENT_CLOSED_INTERVAL]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ content (interval [(a,b)]) = b − a
   
   [CONTENT_CLOSED_INTERVAL_CASES]  Theorem
      
      ⊢ ∀a b. content (interval [(a,b)]) = if a ≤ b then b − a else 0
   
   [CONTENT_DOUBLESPLIT]  Theorem
      
      ⊢ ∀a b c e.
          0 < e ⇒
          ∃d. 0 < d ∧
              content (interval [(a,b)] ∩ {x | abs (x − c) ≤ d}) < e
   
   [CONTENT_EMPTY]  Theorem
      
      ⊢ content ∅ = 0
   
   [CONTENT_EQ_0]  Theorem
      
      ⊢ ∀a b. content (interval [(a,b)]) = 0 ⇔ b ≤ a
   
   [CONTENT_EQ_0_1]  Theorem
      
      ⊢ ∀a b. content (interval [(a,b)]) = 0 ⇔ b ≤ a
   
   [CONTENT_EQ_0_GEN]  Theorem
      
      ⊢ ∀s. bounded s ⇒ (content s = 0 ⇔ ∃a. ∀x. x ∈ s ⇒ x = a)
   
   [CONTENT_EQ_0_INTERIOR]  Theorem
      
      ⊢ ∀a b.
          content (interval [(a,b)]) = 0 ⇔ interior (interval [(a,b)]) = ∅
   
   [CONTENT_IMAGE_AFFINITY_INTERVAL]  Theorem
      
      ⊢ ∀a b m c.
          content (IMAGE (λx. m * x + c) (interval [(a,b)])) =
          abs m pow 1 * content (interval [(a,b)])
   
   [CONTENT_IMAGE_STRETCH_INTERVAL]  Theorem
      
      ⊢ ∀a b m.
          content (IMAGE (λx. m 1 * x) (interval [(a,b)])) =
          abs (product (1 .. 1) m) * content (interval [(a,b)])
   
   [CONTENT_LT_NZ]  Theorem
      
      ⊢ ∀a b.
          0 < content (interval [(a,b)]) ⇔ content (interval [(a,b)]) ≠ 0
   
   [CONTENT_POS_LE]  Theorem
      
      ⊢ ∀a b. 0 ≤ content (interval [(a,b)])
   
   [CONTENT_POS_LT]  Theorem
      
      ⊢ ∀a b. a < b ⇒ 0 < content (interval [(a,b)])
   
   [CONTENT_POS_LT_EQ]  Theorem
      
      ⊢ ∀a b. 0 < content (interval [(a,b)]) ⇔ a < b
   
   [CONTENT_SPLIT]  Theorem
      
      ⊢ ∀a b k.
          content (interval [(a,b)]) =
          content (interval [(a,b)] ∩ {x | x ≤ c}) +
          content (interval [(a,b)] ∩ {x | x ≥ c})
   
   [CONTENT_SUBSET]  Theorem
      
      ⊢ ∀a b c d.
          interval [(a,b)] ⊆ interval [(c,d)] ⇒
          content (interval [(a,b)]) ≤ content (interval [(c,d)])
   
   [CONTENT_UNIT]  Theorem
      
      ⊢ content (interval [(0,1)]) = 1
   
   [CONTINUOUS_ON_VECTOR_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ∧
          f continuous_on interval [(a,b)] ⇒
          (λx. vector_variation (interval [(a,x)]) f) continuous_on
          interval [(a,b)]
   
   [CONVEX_CONTAINS_SEGMENT]  Theorem
      
      ⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s
   
   [DECREASING_BOUNDED_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ⇒
          f has_bounded_variation_on interval [(a,b)]
   
   [DECREASING_BOUNDED_VARIATION_GEN]  Theorem
      
      ⊢ ∀f s.
          bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f y ≤ f x) ⇒
          f has_bounded_variation_on s
   
   [DECREASING_LEFT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ∧ c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(a,c)])
   
   [DECREASING_RIGHT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ∧ c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(c,b)])
   
   [DECREASING_VECTOR_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          interval [(a,b)] ≠ ∅ ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ⇒
          vector_variation (interval [(a,b)]) f = f a − f b
   
   [DIVISION_1_SORT]  Theorem
      
      ⊢ ∀d s.
          d division_of s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
          ∃n t.
            IMAGE t (1 .. n) = d ∧
            ∀i j.
              i ∈ 1 .. n ∧ j ∈ 1 .. n ∧ i < j ⇒
              t i ≠ t j ∧ ∀x y. x ∈ t i ∧ y ∈ t j ⇒ x ≤ y
   
   [DIVISION_COMMON_POINT_BOUND]  Theorem
      
      ⊢ ∀d s x.
          d division_of s ⇒
          CARD {k | k ∈ d ∧ content k ≠ 0 ∧ x ∈ k} ≤ 2 ** 1
   
   [DIVISION_CONTAINS]  Theorem
      
      ⊢ ∀s i. s division_of i ⇒ ∀x. x ∈ i ⇒ ∃k. x ∈ k ∧ k ∈ s
   
   [DIVISION_DISJOINT_UNION]  Theorem
      
      ⊢ ∀s1 s2 p1 p2.
          p1 division_of s1 ∧ p2 division_of s2 ∧
          interior s1 ∩ interior s2 = ∅ ⇒
          p1 ∪ p2 division_of s1 ∪ s2
   
   [DIVISION_DOUBLESPLIT]  Theorem
      
      ⊢ ∀p a b c e.
          p division_of interval [(a,b)] ⇒
          {l ∩ {x | abs (x − c) ≤ e} |
           l |
           l ∈ p ∧ l ∩ {x | abs (x − c) ≤ e} ≠ ∅} division_of
          interval [(a,b)] ∩ {x | abs (x − c) ≤ e}
   
   [DIVISION_INTER]  Theorem
      
      ⊢ ∀s1 s2 p1 p2.
          p1 division_of s1 ∧ p2 division_of s2 ⇒
          {k1 ∩ k2 | k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ ∅} division_of s1 ∩ s2
   
   [DIVISION_INTER_1]  Theorem
      
      ⊢ ∀d i a b.
          d division_of i ∧ interval [(a,b)] ⊆ i ⇒
          {interval [(a,b)] ∩ k | k | k ∈ d ∧ interval [(a,b)] ∩ k ≠ ∅} division_of
          interval [(a,b)]
   
   [DIVISION_OF]  Theorem
      
      ⊢ ∀s i.
          s division_of i ⇔
          FINITE s ∧ (∀k. k ∈ s ⇒ k ≠ ∅ ∧ ∃a b. k = interval [(a,b)]) ∧
          (∀k1 k2.
             k1 ∈ s ∧ k2 ∈ s ∧ k1 ≠ k2 ⇒ interior k1 ∩ interior k2 = ∅) ∧
          BIGUNION s = i
   
   [DIVISION_OF_AFFINITY]  Theorem
      
      ⊢ ∀d s m c.
          IMAGE (IMAGE (λx. m * x + c)) d division_of
          IMAGE (λx. m * x + c) s ⇔
          if m = 0 then if s = ∅ then d = ∅ else d ≠ ∅ ∧ ∀k. k ∈ d ⇒ k ≠ ∅
          else d division_of s
   
   [DIVISION_OF_BIGUNION]  Theorem
      
      ⊢ ∀f. FINITE f ∧ (∀p. p ∈ f ⇒ p division_of BIGUNION p) ∧
            (∀k1 k2.
               k1 ∈ BIGUNION f ∧ k2 ∈ BIGUNION f ∧ k1 ≠ k2 ⇒
               interior k1 ∩ interior k2 = ∅) ⇒
            BIGUNION f division_of BIGUNION (BIGUNION f)
   
   [DIVISION_OF_CLOSED]  Theorem
      
      ⊢ ∀s i. s division_of i ⇒ closed i
   
   [DIVISION_OF_CONTENT_0]  Theorem
      
      ⊢ ∀a b d.
          content (interval [(a,b)]) = 0 ∧ d division_of interval [(a,b)] ⇒
          ∀k. k ∈ d ⇒ content k = 0
   
   [DIVISION_OF_FINITE]  Theorem
      
      ⊢ ∀s i. s division_of i ⇒ FINITE s
   
   [DIVISION_OF_NONTRIVIAL]  Theorem
      
      ⊢ ∀s a b.
          s division_of interval [(a,b)] ∧ content (interval [(a,b)]) ≠ 0 ⇒
          {k | k ∈ s ∧ content k ≠ 0} division_of interval [(a,b)]
   
   [DIVISION_OF_REFLECT]  Theorem
      
      ⊢ ∀d s.
          IMAGE (IMAGE (λx. -x)) d division_of IMAGE (λx. -x) s ⇔
          d division_of s
   
   [DIVISION_OF_SELF]  Theorem
      
      ⊢ ∀a b.
          interval [(a,b)] ≠ ∅ ⇒
          {interval [(a,b)]} division_of interval [(a,b)]
   
   [DIVISION_OF_SING]  Theorem
      
      ⊢ ∀s a. s division_of interval [(a,a)] ⇔ s = {interval [(a,a)]}
   
   [DIVISION_OF_SUBSET]  Theorem
      
      ⊢ ∀p q. p division_of BIGUNION p ∧ q ⊆ p ⇒ q division_of BIGUNION q
   
   [DIVISION_OF_TAGGED_DIVISION]  Theorem
      
      ⊢ ∀s i. s tagged_division_of i ⇒ IMAGE SND s division_of i
   
   [DIVISION_OF_TRANSLATION]  Theorem
      
      ⊢ ∀d s.
          IMAGE (IMAGE (λx. a + x)) d division_of IMAGE (λx. a + x) s ⇔
          d division_of s
   
   [DIVISION_OF_TRIVIAL]  Theorem
      
      ⊢ ∀s. s division_of ∅ ⇔ s = ∅
   
   [DIVISION_OF_UNION_SELF]  Theorem
      
      ⊢ ∀p s. p division_of s ⇒ p division_of BIGUNION p
   
   [DIVISION_POINTS_FINITE]  Theorem
      
      ⊢ ∀d i. d division_of i ⇒ FINITE (division_points i d)
   
   [DIVISION_POINTS_PSUBSET]  Theorem
      
      ⊢ ∀a b c d.
          d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ∧
          (∃l. l ∈ d ∧
               (interval_lowerbound l = c ∨ interval_upperbound l = c)) ⇒
          division_points (interval [(a,b)] ∩ {x | x ≤ c})
            {l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊂
          division_points (interval [(a,b)]) d ∧
          division_points (interval [(a,b)] ∩ {x | x ≥ c})
            {l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊂
          division_points (interval [(a,b)]) d
   
   [DIVISION_POINTS_SUBSET]  Theorem
      
      ⊢ ∀a b c d k.
          d division_of interval [(a,b)] ∧ a < b ∧ a < c ∧ c < b ⇒
          division_points (interval [(a,b)] ∩ {x | x ≤ c})
            {l ∩ {x | x ≤ c} | l | l ∈ d ∧ l ∩ {x | x ≤ c} ≠ ∅} ⊆
          division_points (interval [(a,b)]) d ∧
          division_points (interval [(a,b)] ∩ {x | x ≥ c})
            {l ∩ {x | x ≥ c} | l | l ∈ d ∧ l ∩ {x | x ≥ c} ≠ ∅} ⊆
          division_points (interval [(a,b)]) d
   
   [DIVISION_SPLIT]  Theorem
      
      ⊢ ∀p a b c.
          p division_of interval [(a,b)] ⇒
          {l ∩ {x | x ≤ c} | l | l ∈ p ∧ l ∩ {x | x ≤ c} ≠ ∅} division_of
          interval [(a,b)] ∩ {x | x ≤ c} ∧
          {l ∩ {x | x ≥ c} | l | l ∈ p ∧ l ∩ {x | x ≥ c} ≠ ∅} division_of
          interval [(a,b)] ∩ {x | x ≥ c}
   
   [DIVISION_SPLIT_LEFT_INJ]  Theorem
      
      ⊢ ∀d i k1 k2 k c.
          d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
          k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
          content (k1 ∩ {x | x ≤ c}) = 0
   
   [DIVISION_SPLIT_LEFT_RIGHT_INJ]  Theorem
      
      ⊢ (∀d i k1 k2 k c.
           d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
           k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
           content (k1 ∩ {x | x ≤ c}) = 0) ∧
        ∀d i k1 k2 k c.
          d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
          k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
          content (k1 ∩ {x | x ≥ c}) = 0
   
   [DIVISION_SPLIT_RIGHT_INJ]  Theorem
      
      ⊢ ∀d i k1 k2 k c.
          d division_of i ∧ k1 ∈ d ∧ k2 ∈ d ∧ k1 ≠ k2 ∧
          k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
          content (k1 ∩ {x | x ≥ c}) = 0
   
   [DIVISION_UNION_INTERVALS_EXISTS]  Theorem
      
      ⊢ ∀a b c d.
          interval [(a,b)] ≠ ∅ ⇒
          ∃p. interval [(a,b)] INSERT p division_of
              interval [(a,b)] ∪ interval [(c,d)]
   
   [DOMINATED_CONVERGENCE]  Theorem
      
      ⊢ ∀f g h s.
          (∀k. f k integrable_on s) ∧ h integrable_on s ∧
          (∀k x. x ∈ s ⇒ abs (f k x) ≤ h x) ∧
          (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [DOMINATED_CONVERGENCE_ABSOLUTELY_INTEGRABLE]  Theorem
      
      ⊢ ∀f g h s.
          (∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
          (∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
          (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
          g absolutely_integrable_on s
   
   [DOMINATED_CONVERGENCE_AE]  Theorem
      
      ⊢ ∀f g h s t.
          (∀k. f k integrable_on s) ∧ h integrable_on s ∧ negligible t ∧
          (∀k x. x ∈ s DIFF t ⇒ abs (f k x) ≤ h x) ∧
          (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [DOMINATED_CONVERGENCE_INTEGRABLE]  Theorem
      
      ⊢ ∀f g h s.
          (∀k. f k absolutely_integrable_on s) ∧ h integrable_on s ∧
          (∀k x. x ∈ s ⇒ abs (g x) ≤ h x) ∧
          (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ⇒
          g integrable_on s
   
   [DROP_INDICATOR]  Theorem
      
      ⊢ ∀s x. indicator s x = if x ∈ s then 1 else 0
   
   [DROP_INDICATOR_ABS_LE_1]  Theorem
      
      ⊢ ∀s x. abs (indicator s x) ≤ 1
   
   [DROP_INDICATOR_LE_1]  Theorem
      
      ⊢ ∀s x. indicator s x ≤ 1
   
   [DROP_INDICATOR_POS_LE]  Theorem
      
      ⊢ ∀s x. 0 ≤ indicator s x
   
   [DSUM_BOUND]  Theorem
      
      ⊢ ∀p a b c e.
          p division_of interval [(a,b)] ∧ abs c ≤ e ⇒
          abs (sum p (λl. content l * c)) ≤ e * content (interval [(a,b)])
   
   [ELEMENTARY_BIGINTER]  Theorem
      
      ⊢ ∀f. FINITE f ∧ f ≠ ∅ ∧ (∀s. s ∈ f ⇒ ∃p. p division_of s) ⇒
            ∃p. p division_of BIGINTER f
   
   [ELEMENTARY_BIGUNION_INTERVALS]  Theorem
      
      ⊢ ∀f. FINITE f ∧ (∀s. s ∈ f ⇒ ∃a b. s = interval [(a,b)]) ⇒
            ∃p. p division_of BIGUNION f
   
   [ELEMENTARY_BOUNDED]  Theorem
      
      ⊢ ∀s. (∃p. p division_of s) ⇒ bounded s
   
   [ELEMENTARY_COMPACT]  Theorem
      
      ⊢ ∀s. (∃d. d division_of s) ⇒ compact s
   
   [ELEMENTARY_EMPTY]  Theorem
      
      ⊢ ∃p. p division_of ∅
   
   [ELEMENTARY_INTER]  Theorem
      
      ⊢ ∀s t.
          (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒
          ∃p. p division_of s ∩ t
   
   [ELEMENTARY_INTERVAL]  Theorem
      
      ⊢ ∀a b. ∃p. p division_of interval [(a,b)]
   
   [ELEMENTARY_SUBSET_INTERVAL]  Theorem
      
      ⊢ ∀s. (∃p. p division_of s) ⇒ ∃a b. s ⊆ interval [(a,b)]
   
   [ELEMENTARY_UNION]  Theorem
      
      ⊢ ∀s t.
          (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒
          ∃p. p division_of s ∪ t
   
   [ELEMENTARY_UNION_INTERVAL]  Theorem
      
      ⊢ ∀p a b.
          p division_of BIGUNION p ⇒
          ∃q. q division_of interval [(a,b)] ∪ BIGUNION p
   
   [ELEMENTARY_UNION_INTERVAL_STRONG]  Theorem
      
      ⊢ ∀p a b.
          p division_of BIGUNION p ⇒
          ∃q. p ⊆ q ∧ q division_of interval [(a,b)] ∪ BIGUNION p
   
   [EMPTY_DIVISION_OF]  Theorem
      
      ⊢ ∀s. ∅ division_of s ⇔ s = ∅
   
   [EQUIINTEGRABLE_ADD]  Theorem
      
      ⊢ ∀fs gs s.
          fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
          {(λx. f x + g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s
   
   [EQUIINTEGRABLE_CLOSED_INTERVAL_RESTRICTIONS]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          {(λx. if x ∈ interval [(c,d)] then f x else 0) |
           c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on interval [(a,b)]
   
   [EQUIINTEGRABLE_CMUL]  Theorem
      
      ⊢ ∀fs s k.
          fs equiintegrable_on s ⇒
          {(λx. c * f x) | abs c ≤ k ∧ f ∈ fs} equiintegrable_on s
   
   [EQUIINTEGRABLE_DIVISION]  Theorem
      
      ⊢ ∀fs d a b.
          d division_of interval [(a,b)] ⇒
          (fs equiintegrable_on interval [(a,b)] ⇔
           ∀i. i ∈ d ⇒ fs equiintegrable_on i)
   
   [EQUIINTEGRABLE_EQ]  Theorem
      
      ⊢ ∀fs gs s.
          fs equiintegrable_on s ∧
          (∀g. g ∈ gs ⇒ ∃f. f ∈ fs ∧ ∀x. x ∈ s ⇒ f x = g x) ⇒
          gs equiintegrable_on s
   
   [EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GE]  Theorem
      
      ⊢ ∀fs f a b.
          fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
          (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
          {(λx. if x ≥ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_GT]  Theorem
      
      ⊢ ∀fs f a b.
          fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
          (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
          {(λx. if x > c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LE]  Theorem
      
      ⊢ ∀fs f a b.
          fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
          (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
          {(λx. if x ≤ c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_HALFSPACE_RESTRICTIONS_LT]  Theorem
      
      ⊢ ∀fs f a b.
          fs equiintegrable_on interval [(a,b)] ∧ f ∈ fs ∧
          (∀h x. h ∈ fs ∧ x ∈ interval [(a,b)] ⇒ abs (h x) ≤ abs (f x)) ⇒
          {(λx. if x < c then h x else 0) | c ∈ 𝕌(:real) ∧ h ∈ fs} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_LIMIT]  Theorem
      
      ⊢ ∀f g a b.
          {f n | n ∈ 𝕌(:num)} equiintegrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ ((λn. f n x) ⟶ g x) sequentially) ⇒
          g integrable_on interval [(a,b)] ∧
          ((λn. integral (interval [(a,b)]) (f n)) ⟶
           integral (interval [(a,b)]) g) sequentially
   
   [EQUIINTEGRABLE_NEG]  Theorem
      
      ⊢ ∀fs s.
          fs equiintegrable_on s ⇒
          {(λx. -f x) | f ∈ fs} equiintegrable_on s
   
   [EQUIINTEGRABLE_ON_NULL]  Theorem
      
      ⊢ ∀fs a b.
          content (interval [(a,b)]) = 0 ⇒
          fs equiintegrable_on interval [(a,b)]
   
   [EQUIINTEGRABLE_ON_SING]  Theorem
      
      ⊢ ∀f a b.
          {f} equiintegrable_on interval [(a,b)] ⇔
          f integrable_on interval [(a,b)]
   
   [EQUIINTEGRABLE_ON_SPLIT]  Theorem
      
      ⊢ ∀fs k a b c.
          fs equiintegrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
          fs equiintegrable_on interval [(a,b)] ∩ {x | x ≥ c} ⇒
          fs equiintegrable_on interval [(a,b)]
   
   [EQUIINTEGRABLE_OPEN_INTERVAL_RESTRICTIONS]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          {(λx. if x ∈ interval (c,d) then f x else 0) |
           c ∈ 𝕌(:real) ∧ d ∈ 𝕌(:real)} equiintegrable_on interval [(a,b)]
   
   [EQUIINTEGRABLE_REFLECT]  Theorem
      
      ⊢ ∀fs a b.
          fs equiintegrable_on interval [(a,b)] ⇒
          {(λx. f (-x)) | f ∈ fs} equiintegrable_on interval [(-b,-a)]
   
   [EQUIINTEGRABLE_SUB]  Theorem
      
      ⊢ ∀fs gs s.
          fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
          {(λx. f x − g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s
   
   [EQUIINTEGRABLE_SUBSET]  Theorem
      
      ⊢ ∀fs gs s. fs equiintegrable_on s ∧ gs ⊆ fs ⇒ gs equiintegrable_on s
   
   [EQUIINTEGRABLE_SUM]  Theorem
      
      ⊢ ∀fs a b.
          fs equiintegrable_on interval [(a,b)] ⇒
          {(λx. sum t (λi. c i * f i x)) |
           FINITE t ∧ (∀i. i ∈ t ⇒ 0 ≤ c i ∧ f i ∈ fs) ∧ sum t c = 1} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_UNIFORM_LIMIT]  Theorem
      
      ⊢ ∀fs a b.
          fs equiintegrable_on interval [(a,b)] ⇒
          {g |
           ∀e. 0 < e ⇒
               ∃f. f ∈ fs ∧ ∀x. x ∈ interval [(a,b)] ⇒ abs (g x − f x) < e} equiintegrable_on
          interval [(a,b)]
   
   [EQUIINTEGRABLE_UNION]  Theorem
      
      ⊢ ∀fs gs s.
          fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
          fs ∪ gs equiintegrable_on s
   
   [FATOU]  Theorem
      
      ⊢ ∀f g s t B.
          negligible t ∧ (∀n. f n integrable_on s) ∧
          (∀n x. x ∈ s DIFF t ⇒ 0 ≤ f n x) ∧
          (∀x. x ∈ s DIFF t ⇒ ((λn. f n x) ⟶ g x) sequentially) ∧
          (∀n. integral s (f n) ≤ B) ⇒
          g integrable_on s ∧ 0 ≤ integral s g ∧ integral s g ≤ B
   
   [FINE_BIGINTER]  Theorem
      
      ⊢ ∀f s p.
          (λx. BIGINTER {f d x | d ∈ s}) FINE p ⇔ ∀d. d ∈ s ⇒ f d FINE p
   
   [FINE_BIGUNION]  Theorem
      
      ⊢ ∀d ps. (∀p. p ∈ ps ⇒ d FINE p) ⇒ d FINE BIGUNION ps
   
   [FINE_DIVISION_EXISTS]  Theorem
      
      ⊢ ∀g a b.
          gauge g ⇒ ∃p. p tagged_division_of interval [(a,b)] ∧ g FINE p
   
   [FINE_INTER]  Theorem
      
      ⊢ ∀p d1 d2. (λx. d1 x ∩ d2 x) FINE p ⇔ d1 FINE p ∧ d2 FINE p
   
   [FINE_SUBSET]  Theorem
      
      ⊢ ∀d p q. p ⊆ q ∧ d FINE q ⇒ d FINE p
   
   [FINE_UNION]  Theorem
      
      ⊢ ∀d p1 p2. d FINE p1 ∧ d FINE p2 ⇒ d FINE p1 ∪ p2
   
   [FINITE_POWERSET]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}
   
   [FLOOR_POS]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ ∃n. flr x = n
   
   [FORALL_IN_DIVISION]  Theorem
      
      ⊢ ∀P d i.
          d division_of i ⇒
          ((∀x. x ∈ d ⇒ P x) ⇔
           ∀a b. interval [(a,b)] ∈ d ⇒ P (interval [(a,b)]))
   
   [FORALL_IN_DIVISION_NONEMPTY]  Theorem
      
      ⊢ ∀P d i.
          d division_of i ⇒
          ((∀x. x ∈ d ⇒ P x) ⇔
           ∀a b.
             interval [(a,b)] ∈ d ∧ interval [(a,b)] ≠ ∅ ⇒
             P (interval [(a,b)]))
   
   [FUNDAMENTAL_THEOREM_OF_CALCULUS]  Theorem
      
      ⊢ ∀f f' a b.
          a ≤ b ∧
          (∀x. x ∈ interval [(a,b)] ⇒
               (f has_vector_derivative f' x)
                 (at x within interval [(a,b)])) ⇒
          (f' has_integral f b − f a) (interval [(a,b)])
   
   [FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR]  Theorem
      
      ⊢ ∀f f' a b.
          a ≤ b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ (f has_vector_derivative f' x) (at x)) ⇒
          (f' has_integral f b − f a) (interval [(a,b)])
   
   [FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG]  Theorem
      
      ⊢ ∀f f' s a b.
          COUNTABLE s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) DIFF s ⇒
               (f has_vector_derivative f' x) (at x)) ⇒
          (f' has_integral f b − f a) (interval [(a,b)])
   
   [FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG]  Theorem
      
      ⊢ ∀f f' s a b.
          COUNTABLE s ∧ a ≤ b ∧ f continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] DIFF s ⇒
               (f has_vector_derivative f' x)
                 (at x within interval [(a,b)])) ⇒
          (f' has_integral f b − f a) (interval [(a,b)])
   
   [GAUGE_BALL]  Theorem
      
      ⊢ ∀e. 0 < e ⇒ gauge (λx. ball (x,e))
   
   [GAUGE_BALL_DEPENDENT]  Theorem
      
      ⊢ ∀e. (∀x. 0 < e x) ⇒ gauge (λx. ball (x,e x))
   
   [GAUGE_BIGINTER]  Theorem
      
      ⊢ ∀f s.
          FINITE s ∧ (∀d. d ∈ s ⇒ gauge (f d)) ⇒
          gauge (λx. BIGINTER {f d x | d ∈ s})
   
   [GAUGE_EXISTENCE_LEMMA]  Theorem
      
      ⊢ ∀p q. (∀x. ∃d. p x ⇒ 0 < d ∧ q d x) ⇔ ∀x. ∃d. 0 < d ∧ (p x ⇒ q d x)
   
   [GAUGE_INTER]  Theorem
      
      ⊢ ∀d1 d2. gauge d1 ∧ gauge d2 ⇒ gauge (λx. d1 x ∩ d2 x)
   
   [GAUGE_MODIFY]  Theorem
      
      ⊢ ∀f. (∀s. open s ⇒ open {x | f x ∈ s}) ⇒
            ∀d. gauge d ⇒ gauge (λx y. d (f x) (f y))
   
   [GAUGE_TRIVIAL]  Theorem
      
      ⊢ gauge (λx. ball (x,1))
   
   [HAS_BOUNDED_SETVARIATION_COMPARISON]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧
          (∀a b.
             interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
             abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
          g has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ⇔
          ∃B. 0 < B ∧
              ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B
   
   [HAS_BOUNDED_SETVARIATION_ON_0]  Theorem
      
      ⊢ ∀s. (λx. 0) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_ABS]  Theorem
      
      ⊢ ∀f s.
          (λx. abs (f x)) has_bounded_setvariation_on s ⇔
          f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_ADD]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
          (λx. f x + g x) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_CMUL]  Theorem
      
      ⊢ ∀f c s.
          f has_bounded_setvariation_on s ⇒
          (λx. c * f x) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ⇔
          (λk. f k) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_COMPOSE_LINEAR]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧ linear g ⇒
          g ∘ f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_DIVISION]  Theorem
      
      ⊢ ∀f a b d.
          operative $+ f ∧ d division_of interval [(a,b)] ⇒
          ((∀k. k ∈ d ⇒ f has_bounded_setvariation_on k) ⇔
           f has_bounded_setvariation_on interval [(a,b)])
   
   [HAS_BOUNDED_SETVARIATION_ON_ELEMENTARY]  Theorem
      
      ⊢ ∀f s.
          (∃d. d division_of s) ⇒
          (f has_bounded_setvariation_on s ⇔
           ∃B. ∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B)
   
   [HAS_BOUNDED_SETVARIATION_ON_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀a b.
             interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
             f (interval [(a,b)]) = g (interval [(a,b)])) ∧
          f has_bounded_setvariation_on s ⇒
          g has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ⇒
          bounded {f (interval [(c,d)]) | interval [(c,d)] ⊆ s}
   
   [HAS_BOUNDED_SETVARIATION_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_setvariation_on interval [(a,b)] ⇔
          ∃B. ∀d.
            d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B
   
   [HAS_BOUNDED_SETVARIATION_ON_NEG]  Theorem
      
      ⊢ ∀f s.
          (λx. -f x) has_bounded_setvariation_on s ⇔
          f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_NULL]  Theorem
      
      ⊢ ∀f s.
          (∀a b. content (interval [(a,b)]) = 0 ⇒ f (interval [(a,b)]) = 0) ∧
          content s = 0 ∧ bounded s ⇒
          f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_SUB]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
          (λx. f x − g x) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_SUBSET]  Theorem
      
      ⊢ ∀f s t.
          f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
          f has_bounded_setvariation_on t
   
   [HAS_BOUNDED_SETVARIATION_ON_SUM]  Theorem
      
      ⊢ ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
          (λx. sum k (λi. f i x)) has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_ON_SUM_AND_SET_VARIATION_SUM_LE]  Theorem
      
      ⊢ (∀f s k.
           FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
           (λx. sum k (λi. f i x)) has_bounded_setvariation_on s) ∧
        ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
          set_variation s (λx. sum k (λi. f i x)) ≤
          sum k (λi. set_variation s (f i))
   
   [HAS_BOUNDED_SETVARIATION_ON_UNIV]  Theorem
      
      ⊢ ∀f. f has_bounded_setvariation_on 𝕌(:real) ⇔
            ∃B. ∀d. d division_of BIGUNION d ⇒ sum d (λk. abs (f k)) ≤ B
   
   [HAS_BOUNDED_SETVARIATION_REFLECT2_EQ]  Theorem
      
      ⊢ ∀f s.
          (λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on
          IMAGE (λx. -x) s ⇔ f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_REFLECT2_EQ_AND_SET_VARIATION_REFLECT2]  Theorem
      
      ⊢ (∀f s.
           (λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on
           IMAGE (λx. -x) s ⇔ f has_bounded_setvariation_on s) ∧
        ∀f s.
          set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
          set_variation s f
   
   [HAS_BOUNDED_SETVARIATION_TRANSLATION]  Theorem
      
      ⊢ ∀f s a.
          f has_bounded_setvariation_on s ⇒
          (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
          IMAGE (λx. -a + x) s
   
   [HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ]  Theorem
      
      ⊢ ∀a f s.
          (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
          IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s
   
   [HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ_AND_SET_VARIATION_TRANSLATION2]  Theorem
      
      ⊢ (∀a f s.
           (λk. f (IMAGE (λx. a + x) k)) has_bounded_setvariation_on
           IMAGE (λx. -a + x) s ⇔ f has_bounded_setvariation_on s) ∧
        ∀a f s.
          set_variation (IMAGE (λx. -a + x) s)
            (λk. f (IMAGE (λx. a + x) k)) =
          set_variation s f
   
   [HAS_BOUNDED_SETVARIATION_WORKS]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ⇒
          (∀d t.
             d division_of t ∧ t ⊆ s ⇒
             sum d (λk. abs (f k)) ≤ set_variation s f) ∧
          ∀B. (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
              set_variation s f ≤ B
   
   [HAS_BOUNDED_SETVARIATION_WORKS_ON_ELEMENTARY]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_setvariation_on s ∧ (∃d. d division_of s) ⇒
          (∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ set_variation s f) ∧
          ∀B. (∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
              set_variation s f ≤ B
   
   [HAS_BOUNDED_SETVARIATION_WORKS_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_setvariation_on interval [(a,b)] ⇒
          (∀d. d division_of interval [(a,b)] ⇒
               sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f) ∧
          ∀B. (∀d. d division_of interval [(a,b)] ⇒
                   sum d (λk. abs (f k)) ≤ B) ⇒
              set_variation (interval [(a,b)]) f ≤ B
   
   [HAS_BOUNDED_VARIATION_AFFINITY2_EQ]  Theorem
      
      ⊢ ∀m c f s.
          (λx. f (m * x + c)) has_bounded_variation_on
          IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
          m = 0 ∨ f has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_AFFINITY2_EQ_AND_VECTOR_VARIATION_AFFINITY2]  Theorem
      
      ⊢ (∀m c f s.
           (λx. f (m * x + c)) has_bounded_variation_on
           IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s ⇔
           m = 0 ∨ f has_bounded_variation_on s) ∧
        ∀m c f s.
          vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s)
            (λx. f (m * x + c)) =
          if m = 0 then 0 else vector_variation s f
   
   [HAS_BOUNDED_VARIATION_AFFINITY_EQ]  Theorem
      
      ⊢ ∀m c f s.
          (λx. f (m * x + c)) has_bounded_variation_on s ⇔
          m = 0 ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s
   
   [HAS_BOUNDED_VARIATION_AFFINITY_EQ_AND_VECTOR_VARIATION_AFFINITY]  Theorem
      
      ⊢ (∀m c f s.
           (λx. f (m * x + c)) has_bounded_variation_on s ⇔
           m = 0 ∨ f has_bounded_variation_on IMAGE (λx. m * x + c) s) ∧
        ∀m c f s.
          vector_variation s (λx. f (m * x + c)) =
          if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f
   
   [HAS_BOUNDED_VARIATION_COMPARISON]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧
          (∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
          g has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_COMPOSE_DECREASING]  Theorem
      
      ⊢ ∀f g a b.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ∧ g has_bounded_variation_on interval [(f b,f a)] ⇒
          g ∘ f has_bounded_variation_on interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_COMPOSE_INCREASING]  Theorem
      
      ⊢ ∀f g a b.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ∧ g has_bounded_variation_on interval [(f a,f b)] ⇒
          g ∘ f has_bounded_variation_on interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_DARBOUX]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ⇔
          ∃g h.
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
               g x ≤ g y) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
               h x ≤ h y) ∧ ∀x. f x = g x − h x
   
   [HAS_BOUNDED_VARIATION_DARBOUX_STRICT]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ⇔
          ∃g h.
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
               g x < g y) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
               h x < h y) ∧ ∀x. f x = g x − h x
   
   [HAS_BOUNDED_VARIATION_DARBOUX_STRONG]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ⇒
          ∃g h.
            (∀x. f x = g x − h x) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
               g x ≤ g y) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
               h x ≤ h y) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
               g x < g y) ∧
            (∀x y.
               x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x < y ⇒
               h x < h y) ∧
            (∀x. x ∈ interval [(a,b)] ∧
                 f continuous (at x within interval [(a,x)]) ⇒
                 g continuous (at x within interval [(a,x)]) ∧
                 h continuous (at x within interval [(a,x)])) ∧
            (∀x. x ∈ interval [(a,b)] ∧
                 f continuous (at x within interval [(x,b)]) ⇒
                 g continuous (at x within interval [(x,b)]) ∧
                 h continuous (at x within interval [(x,b)])) ∧
            ∀x. x ∈ interval [(a,b)] ∧
                f continuous (at x within interval [(a,b)]) ⇒
                g continuous (at x within interval [(a,b)]) ∧
                h continuous (at x within interval [(a,b)])
   
   [HAS_BOUNDED_VARIATION_NONTRIVIAL]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇔
          ∃B. ∀d t.
            d division_of t ∧ t ⊆ s ∧ (∀k. k ∈ d ⇒ interior k ≠ ∅) ⇒
            sum d
              (λk.
                   abs
                     (f (interval_upperbound k) − f (interval_lowerbound k))) ≤
            B
   
   [HAS_BOUNDED_VARIATION_ON_ABS]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇒
          (λx. abs (f x)) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_ADD]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
          (λx. f x + g x) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_CLOSURE]  Theorem
      
      ⊢ ∀f s.
          is_interval s ∧ f has_bounded_variation_on s ⇒
          f has_bounded_variation_on closure s
   
   [HAS_BOUNDED_VARIATION_ON_CMUL]  Theorem
      
      ⊢ ∀f c s.
          f has_bounded_variation_on s ⇒
          (λx. c * f x) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_COMBINE]  Theorem
      
      ⊢ ∀f a b c.
          a ≤ c ∧ c ≤ b ⇒
          (f has_bounded_variation_on interval [(a,b)] ⇔
           f has_bounded_variation_on interval [(a,c)] ∧
           f has_bounded_variation_on interval [(c,b)])
   
   [HAS_BOUNDED_VARIATION_ON_COMBINE_GEN]  Theorem
      
      ⊢ ∀f s a.
          is_interval s ⇒
          (f has_bounded_variation_on s ⇔
           f has_bounded_variation_on {x | x ∈ s ∧ x ≤ a} ∧
           f has_bounded_variation_on {x | x ∈ s ∧ x ≥ a})
   
   [HAS_BOUNDED_VARIATION_ON_COMPONENTWISE]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇔
          (λx. f x) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_COMPOSE_LINEAR]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ linear g ⇒
          g ∘ f has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_CONST]  Theorem
      
      ⊢ ∀s c. (λx. c) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_DIVISION]  Theorem
      
      ⊢ ∀f a b d.
          d division_of interval [(a,b)] ⇒
          ((∀k. k ∈ d ⇒ f has_bounded_variation_on k) ⇔
           f has_bounded_variation_on interval [(a,b)])
   
   [HAS_BOUNDED_VARIATION_ON_EMPTY]  Theorem
      
      ⊢ ∀f. f has_bounded_variation_on ∅
   
   [HAS_BOUNDED_VARIATION_ON_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x = g x) ∧ f has_bounded_variation_on s ⇒
          g has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_ID]  Theorem
      
      ⊢ ∀a b. (λx. x) has_bounded_variation_on interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ∧ is_interval s ⇒
          bounded (IMAGE f s)
   
   [HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ⇒
          bounded (IMAGE f (interval [(a,b)]))
   
   [HAS_BOUNDED_VARIATION_ON_IMP_BOUNDED_ON_SUBINTERVALS]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇒
          bounded {f d − f c | interval [(c,d)] ⊆ s ∧ interval [(c,d)] ≠ ∅}
   
   [HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_LEFT]  Theorem
      
      ⊢ ∀f a b.
          f absolutely_integrable_on interval [(a,b)] ⇒
          (λc. integral (interval [(c,b)]) f) has_bounded_variation_on
          interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_ON_INDEFINITE_INTEGRAL_RIGHT]  Theorem
      
      ⊢ ∀f a b.
          f absolutely_integrable_on interval [(a,b)] ⇒
          (λc. integral (interval [(a,c)]) f) has_bounded_variation_on
          interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_ON_MAX]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
          (λx. max (f x) (g x)) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_MIN]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
          (λx. min (f x) (g x)) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_MUL]  Theorem
      
      ⊢ ∀f g a b.
          f has_bounded_variation_on interval [(a,b)] ∧
          g has_bounded_variation_on interval [(a,b)] ⇒
          (λx. f x * g x) has_bounded_variation_on interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_ON_NEG]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on s ⇒
          (λx. -f x) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_NULL]  Theorem
      
      ⊢ ∀f s. content s = 0 ∧ bounded s ⇒ f has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_REFLECT]  Theorem
      
      ⊢ ∀f s.
          f has_bounded_variation_on IMAGE (λx. -x) s ⇒
          (λx. f (-x)) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(-b,-a)] ⇒
          (λx. f (-x)) has_bounded_variation_on interval [(a,b)]
   
   [HAS_BOUNDED_VARIATION_ON_SING]  Theorem
      
      ⊢ ∀f a. f has_bounded_variation_on {a}
   
   [HAS_BOUNDED_VARIATION_ON_SUB]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
          (λx. f x − g x) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_SUBSET]  Theorem
      
      ⊢ ∀f s t.
          f has_bounded_variation_on s ∧ t ⊆ s ⇒
          f has_bounded_variation_on t
   
   [HAS_BOUNDED_VARIATION_ON_SUM]  Theorem
      
      ⊢ ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
          (λx. sum k (λi. f i x)) has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_ON_SUM_AND_SUM_LE]  Theorem
      
      ⊢ (∀f s k.
           FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
           (λx. sum k (λi. f i x)) has_bounded_variation_on s) ∧
        ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
          vector_variation s (λx. sum k (λi. f i x)) ≤
          sum k (λi. vector_variation s (f i))
   
   [HAS_BOUNDED_VARIATION_REFLECT2_EQ]  Theorem
      
      ⊢ ∀f s.
          (λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
          f has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_REFLECT2_EQ_AND_VECTOR_VARIATION_REFLECT2]  Theorem
      
      ⊢ (∀f s.
           (λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
           f has_bounded_variation_on s) ∧
        ∀f s.
          vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) =
          vector_variation s f
   
   [HAS_BOUNDED_VARIATION_REFLECT_EQ]  Theorem
      
      ⊢ ∀f s.
          (λx. f (-x)) has_bounded_variation_on s ⇔
          f has_bounded_variation_on IMAGE (λx. -x) s
   
   [HAS_BOUNDED_VARIATION_REFLECT_EQ_AND_VECTOR_VARIATION_REFLECT]  Theorem
      
      ⊢ (∀f s.
           (λx. f (-x)) has_bounded_variation_on s ⇔
           f has_bounded_variation_on IMAGE (λx. -x) s) ∧
        ∀f s.
          vector_variation s (λx. f (-x)) =
          vector_variation (IMAGE (λx. -x) s) f
   
   [HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL]  Theorem
      
      ⊢ ∀f u v.
          (λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
          f has_bounded_variation_on interval [(-v,-u)]
   
   [HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL_AND_VECTOR_VARIATION_REFLECT_INTERVAL]  Theorem
      
      ⊢ (∀f u v.
           (λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
           f has_bounded_variation_on interval [(-v,-u)]) ∧
        ∀f u v.
          vector_variation (interval [(u,v)]) (λx. f (-x)) =
          vector_variation (interval [(-v,-u)]) f
   
   [HAS_BOUNDED_VARIATION_SUM_LE]  Theorem
      
      ⊢ ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_variation_on s) ⇒
          vector_variation s (λx. sum k (λi. f i x)) ≤
          sum k (λi. vector_variation s (f i))
   
   [HAS_BOUNDED_VARIATION_TRANSLATION]  Theorem
      
      ⊢ ∀f s a.
          f has_bounded_variation_on s ⇒
          (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s
   
   [HAS_BOUNDED_VARIATION_TRANSLATION2_EQ]  Theorem
      
      ⊢ ∀a f s.
          (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
          f has_bounded_variation_on s
   
   [HAS_BOUNDED_VARIATION_TRANSLATION2_EQ_AND_VECTOR_VARIATION_TRANSLATION2]  Theorem
      
      ⊢ (∀a f s.
           (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s ⇔
           f has_bounded_variation_on s) ∧
        ∀a f s.
          vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
          vector_variation s f
   
   [HAS_BOUNDED_VARIATION_TRANSLATION_EQ]  Theorem
      
      ⊢ ∀a f s.
          (λx. f (a + x)) has_bounded_variation_on s ⇔
          f has_bounded_variation_on IMAGE (λx. a + x) s
   
   [HAS_BOUNDED_VARIATION_TRANSLATION_EQ_AND_VECTOR_VARIATION_TRANSLATION]  Theorem
      
      ⊢ (∀a f s.
           (λx. f (a + x)) has_bounded_variation_on s ⇔
           f has_bounded_variation_on IMAGE (λx. a + x) s) ∧
        ∀a f s.
          vector_variation s (λx. f (a + x)) =
          vector_variation (IMAGE (λx. a + x) s) f
   
   [HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL]  Theorem
      
      ⊢ ∀a f u v.
          (λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
          f has_bounded_variation_on interval [(a + u,a + v)]
   
   [HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL_AND_VECTOR_VARIATION_TRANSLATION_INTERVAL]  Theorem
      
      ⊢ (∀a f u v.
           (λx. f (a + x)) has_bounded_variation_on interval [(u,v)] ⇔
           f has_bounded_variation_on interval [(a + u,a + v)]) ∧
        ∀a f u v.
          vector_variation (interval [(u,v)]) (λx. f (a + x)) =
          vector_variation (interval [(a + u,a + v)]) f
   
   [HAS_BOUNDED_VECTOR_VARIATION_LEFT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          f has_bounded_variation_on interval [(a,b)] ∧
          c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(a,c)])
   
   [HAS_BOUNDED_VECTOR_VARIATION_RIGHT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          f has_bounded_variation_on interval [(a,b)] ∧
          c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(c,b)])
   
   [HAS_DERIVATIVE_ZERO_UNIQUE_STRONG_INTERVAL]  Theorem
      
      ⊢ ∀f a b k y.
          COUNTABLE k ∧ f continuous_on interval [(a,b)] ∧ f a = y ∧
          (∀x. x ∈ interval [(a,b)] DIFF k ⇒
               (f has_derivative (λh. 0)) (at x within interval [(a,b)])) ⇒
          ∀x. x ∈ interval [(a,b)] ⇒ f x = y
   
   [HAS_INTEGRAL]  Theorem
      
      ⊢ ∀f i s.
          (f has_integral i) s ⇔
          ∀e. 0 < e ⇒
              ∃B. 0 < B ∧
                  ∀a b.
                    ball (0,B) ⊆ interval [(a,b)] ⇒
                    ∃z. ((λx. if x ∈ s then f x else 0) has_integral z)
                          (interval [(a,b)]) ∧ abs (z − i) < e
   
   [HAS_INTEGRAL_0]  Theorem
      
      ⊢ ∀s. ((λx. 0) has_integral 0) s
   
   [HAS_INTEGRAL_0_EQ]  Theorem
      
      ⊢ ∀i s. ((λx. 0) has_integral i) s ⇔ i = 0
   
   [HAS_INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT]  Theorem
      
      ⊢ ∀f g s i j.
          (f has_integral i) s ∧ (g has_integral j) s ∧
          (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
          abs i ≤ j
   
   [HAS_INTEGRAL_ADD]  Theorem
      
      ⊢ ∀f g s k.
          (f has_integral k) s ∧ (g has_integral l) s ⇒
          ((λx. f x + g x) has_integral k + l) s
   
   [HAS_INTEGRAL_AFFINITY]  Theorem
      
      ⊢ ∀f i a b m c.
          (f has_integral i) (interval [(a,b)]) ∧ m ≠ 0 ⇒
          ((λx. f (m * x + c)) has_integral (abs m pow 1)⁻¹ * i)
            (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)]))
   
   [HAS_INTEGRAL_ALT]  Theorem
      
      ⊢ ∀f s i.
          (f has_integral i) s ⇔
          (∀a b.
             (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
          ∀e. 0 < e ⇒
              ∃B. 0 < B ∧
                  ∀a b.
                    ball (0,B) ⊆ interval [(a,b)] ⇒
                    abs
                      (integral (interval [(a,b)])
                         (λx. if x ∈ s then f x else 0) − i) < e
   
   [HAS_INTEGRAL_BIGUNION]  Theorem
      
      ⊢ ∀f i t.
          FINITE t ∧ (∀s. s ∈ t ⇒ (f has_integral i s) s) ∧
          (∀s s'. s ∈ t ∧ s' ∈ t ∧ s ≠ s' ⇒ negligible (s ∩ s')) ⇒
          (f has_integral sum t i) (BIGUNION t)
   
   [HAS_INTEGRAL_BOUND]  Theorem
      
      ⊢ ∀f a b i B.
          0 ≤ B ∧ (f has_integral i) (interval [(a,b)]) ∧
          (∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ B) ⇒
          abs i ≤ B * content (interval [(a,b)])
   
   [HAS_INTEGRAL_CLOSURE]  Theorem
      
      ⊢ ∀f y s.
          negligible (frontier s) ⇒
          ((f has_integral y) (closure s) ⇔ (f has_integral y) s)
   
   [HAS_INTEGRAL_CMUL]  Theorem
      
      ⊢ ∀f k s c.
          (f has_integral k) s ⇒ ((λx. c * f x) has_integral c * k) s
   
   [HAS_INTEGRAL_COMBINE]  Theorem
      
      ⊢ ∀f i j a b c.
          a ≤ c ∧ c ≤ b ∧ (f has_integral i) (interval [(a,c)]) ∧
          (f has_integral j) (interval [(c,b)]) ⇒
          (f has_integral i + j) (interval [(a,b)])
   
   [HAS_INTEGRAL_COMBINE_DIVISION]  Theorem
      
      ⊢ ∀f s d i.
          d division_of s ∧ (∀k. k ∈ d ⇒ (f has_integral i k) k) ⇒
          (f has_integral sum d i) s
   
   [HAS_INTEGRAL_COMBINE_DIVISION_TOPDOWN]  Theorem
      
      ⊢ ∀f s d k.
          f integrable_on s ∧ d division_of k ∧ k ⊆ s ⇒
          (f has_integral sum d (λi. integral i f)) k
   
   [HAS_INTEGRAL_COMBINE_TAGGED_DIVISION]  Theorem
      
      ⊢ ∀f s p i.
          p tagged_division_of s ∧
          (∀x k. (x,k) ∈ p ⇒ (f has_integral i k) k) ⇒
          (f has_integral sum p (λ(x,k). i k)) s
   
   [HAS_INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN]  Theorem
      
      ⊢ ∀f a b p.
          f integrable_on interval [(a,b)] ∧
          p tagged_division_of interval [(a,b)] ⇒
          (f has_integral sum p (λ(x,k). integral k f)) (interval [(a,b)])
   
   [HAS_INTEGRAL_COMPONENTWISE]  Theorem
      
      ⊢ ∀f s y. (f has_integral y) s ⇔ ((λx. f x) has_integral y) s
   
   [HAS_INTEGRAL_COMPONENT_LBOUND]  Theorem
      
      ⊢ ∀f a b i.
          (f has_integral i) (interval [(a,b)]) ∧
          (∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
          B * content (interval [(a,b)]) ≤ i
   
   [HAS_INTEGRAL_COMPONENT_LE]  Theorem
      
      ⊢ ∀f g s i j.
          (f has_integral i) s ∧ (g has_integral j) s ∧
          (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_COMPONENT_LE_AE]  Theorem
      
      ⊢ ∀f g s i j k t.
          negligible t ∧ (f has_integral i) s ∧ (g has_integral j) s ∧
          (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_COMPONENT_NEG]  Theorem
      
      ⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0
   
   [HAS_INTEGRAL_COMPONENT_POS]  Theorem
      
      ⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i
   
   [HAS_INTEGRAL_COMPONENT_UBOUND]  Theorem
      
      ⊢ ∀f a b i.
          (f has_integral i) (interval [(a,b)]) ∧
          (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
          i ≤ B * content (interval [(a,b)])
   
   [HAS_INTEGRAL_CONST]  Theorem
      
      ⊢ ∀a b c.
          ((λx. c) has_integral content (interval [(a,b)]) * c)
            (interval [(a,b)])
   
   [HAS_INTEGRAL_DIFF]  Theorem
      
      ⊢ ∀f i j s t.
          (f has_integral i) s ∧ (f has_integral j) t ∧
          negligible (t DIFF s) ⇒
          (f has_integral i − j) (s DIFF t)
   
   [HAS_INTEGRAL_DROP_LE]  Theorem
      
      ⊢ ∀f g s i j.
          (f has_integral i) s ∧ (g has_integral j) s ∧
          (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_DROP_NEG]  Theorem
      
      ⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0
   
   [HAS_INTEGRAL_DROP_POS]  Theorem
      
      ⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i
   
   [HAS_INTEGRAL_DROP_POS_AE]  Theorem
      
      ⊢ ∀f s t i.
          (f has_integral i) s ∧ negligible t ∧
          (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
          0 ≤ i
   
   [HAS_INTEGRAL_EMPTY]  Theorem
      
      ⊢ ∀f. (f has_integral 0) ∅
   
   [HAS_INTEGRAL_EMPTY_EQ]  Theorem
      
      ⊢ ∀f i. (f has_integral i) ∅ ⇔ i = 0
   
   [HAS_INTEGRAL_EQ]  Theorem
      
      ⊢ ∀f g k s.
          (∀x. x ∈ s ⇒ f x = g x) ∧ (f has_integral k) s ⇒
          (g has_integral k) s
   
   [HAS_INTEGRAL_EQ_EQ]  Theorem
      
      ⊢ ∀f g k s.
          (∀x. x ∈ s ⇒ f x = g x) ⇒
          ((f has_integral k) s ⇔ (g has_integral k) s)
   
   [HAS_INTEGRAL_FACTOR_CONTENT]  Theorem
      
      ⊢ ∀f i a b.
          (f has_integral i) (interval [(a,b)]) ⇔
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
                      abs (sum p (λ(x,k). content k * f x) − i) ≤
                      e * content (interval [(a,b)])
   
   [HAS_INTEGRAL_INTEGRABLE]  Theorem
      
      ⊢ ∀f i s. (f has_integral i) s ⇒ f integrable_on s
   
   [HAS_INTEGRAL_INTEGRABLE_INTEGRAL]  Theorem
      
      ⊢ ∀f i s. (f has_integral i) s ⇔ f integrable_on s ∧ integral s f = i
   
   [HAS_INTEGRAL_INTEGRAL]  Theorem
      
      ⊢ ∀f s. f integrable_on s ⇔ (f has_integral integral s f) s
   
   [HAS_INTEGRAL_INTERIOR]  Theorem
      
      ⊢ ∀f y s.
          negligible (frontier s) ⇒
          ((f has_integral y) (interior s) ⇔ (f has_integral y) s)
   
   [HAS_INTEGRAL_IS_0]  Theorem
      
      ⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ (f has_integral 0) s
   
   [HAS_INTEGRAL_LE_AE]  Theorem
      
      ⊢ ∀f g s i j t.
          (f has_integral i) s ∧ (g has_integral j) s ∧ negligible t ∧
          (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_LIM_AT_POSINFINITY]  Theorem
      
      ⊢ ∀f l.
          (f has_integral l) {t | 0 ≤ t} ⇔
          (∀a. f integrable_on interval [(0,a)]) ∧
          ((λa. integral (interval [(0,a)]) f) ⟶ l) at_posinfinity
   
   [HAS_INTEGRAL_LIM_SEQUENTIALLY]  Theorem
      
      ⊢ ∀f l.
          (f ⟶ 0) at_posinfinity ∧
          (∀n. f integrable_on interval [(0,&n)]) ∧
          ((λn. integral (interval [(0,&n)]) f) ⟶ l) sequentially ⇒
          (f has_integral l) {t | 0 ≤ t}
   
   [HAS_INTEGRAL_LINEAR]  Theorem
      
      ⊢ ∀f y s h.
          (f has_integral y) s ∧ linear h ⇒ (h ∘ f has_integral h y) s
   
   [HAS_INTEGRAL_NEG]  Theorem
      
      ⊢ ∀f k s. (f has_integral k) s ⇒ ((λx. -f x) has_integral -k) s
   
   [HAS_INTEGRAL_NEGLIGIBLE]  Theorem
      
      ⊢ ∀f s t.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ f x = 0) ⇒
          (f has_integral 0) t
   
   [HAS_INTEGRAL_NEGLIGIBLE_EQ]  Theorem
      
      ⊢ ∀f s.
          (∀x i. x ∈ s ⇒ 0 ≤ f x) ⇒
          ((f has_integral 0) s ⇔ negligible {x | x ∈ s ∧ f x ≠ 0})
   
   [HAS_INTEGRAL_NULL]  Theorem
      
      ⊢ ∀f a b.
          content (interval [(a,b)]) = 0 ⇒
          (f has_integral 0) (interval [(a,b)])
   
   [HAS_INTEGRAL_NULL_EQ]  Theorem
      
      ⊢ ∀f a b i.
          content (interval [(a,b)]) = 0 ⇒
          ((f has_integral i) (interval [(a,b)]) ⇔ i = 0)
   
   [HAS_INTEGRAL_ON_SUPERSET]  Theorem
      
      ⊢ ∀f s t i.
          (∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ (f has_integral i) s ⇒
          (f has_integral i) t
   
   [HAS_INTEGRAL_REFL]  Theorem
      
      ⊢ ∀f a. (f has_integral 0) (interval [(a,a)])
   
   [HAS_INTEGRAL_REFLECT]  Theorem
      
      ⊢ ∀f i a b.
          ((λx. f (-x)) has_integral i) (interval [(-b,-a)]) ⇔
          (f has_integral i) (interval [(a,b)])
   
   [HAS_INTEGRAL_REFLECT_GEN]  Theorem
      
      ⊢ ∀f i s.
          ((λx. f (-x)) has_integral i) s ⇔
          (f has_integral i) (IMAGE (λx. -x) s)
   
   [HAS_INTEGRAL_REFLECT_LEMMA]  Theorem
      
      ⊢ ∀f i a b.
          (f has_integral i) (interval [(a,b)]) ⇒
          ((λx. f (-x)) has_integral i) (interval [(-b,-a)])
   
   [HAS_INTEGRAL_RESTRICT]  Theorem
      
      ⊢ ∀f s t i.
          s ⊆ t ⇒
          (((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
           (f has_integral i) s)
   
   [HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVAL]  Theorem
      
      ⊢ ∀f a b c d i.
          (f has_integral i) (interval [(c,d)]) ∧
          interval [(c,d)] ⊆ interval [(a,b)] ⇒
          ((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
            (interval [(a,b)])
   
   [HAS_INTEGRAL_RESTRICT_CLOSED_SUBINTERVALS_EQ]  Theorem
      
      ⊢ ∀f a b c d i.
          interval [(c,d)] ⊆ interval [(a,b)] ⇒
          (((λx. if x ∈ interval [(c,d)] then f x else 0) has_integral i)
             (interval [(a,b)]) ⇔ (f has_integral i) (interval [(c,d)]))
   
   [HAS_INTEGRAL_RESTRICT_INTER]  Theorem
      
      ⊢ ∀f s t.
          ((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
          (f has_integral i) (s ∩ t)
   
   [HAS_INTEGRAL_RESTRICT_OPEN_SUBINTERVAL]  Theorem
      
      ⊢ ∀f a b c d i.
          (f has_integral i) (interval [(c,d)]) ∧
          interval [(c,d)] ⊆ interval [(a,b)] ⇒
          ((λx. if x ∈ interval (c,d) then f x else 0) has_integral i)
            (interval [(a,b)])
   
   [HAS_INTEGRAL_RESTRICT_UNIV]  Theorem
      
      ⊢ ∀f s i.
          ((λx. if x ∈ s then f x else 0) has_integral i) 𝕌(:real) ⇔
          (f has_integral i) s
   
   [HAS_INTEGRAL_SEPARATE_SIDES]  Theorem
      
      ⊢ ∀f i a b.
          (f has_integral i) (interval [(a,b)]) ⇒
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀p1 p2.
                    p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
                    d FINE p1 ∧
                    p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ∧
                    d FINE p2 ⇒
                    abs
                      (sum p1 (λ(x,k). content k * f x) +
                       sum p2 (λ(x,k). content k * f x) − i) < e
   
   [HAS_INTEGRAL_SPIKE]  Theorem
      
      ⊢ ∀f g s t y.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ∧
          (f has_integral y) t ⇒
          (g has_integral y) t
   
   [HAS_INTEGRAL_SPIKE_EQ]  Theorem
      
      ⊢ ∀f g s t y.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          ((f has_integral y) t ⇔ (g has_integral y) t)
   
   [HAS_INTEGRAL_SPIKE_FINITE]  Theorem
      
      ⊢ ∀f g s t y.
          FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ∧ (f has_integral y) t ⇒
          (g has_integral y) t
   
   [HAS_INTEGRAL_SPIKE_FINITE_EQ]  Theorem
      
      ⊢ ∀f g s t y.
          FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          ((f has_integral y) t ⇔ (g has_integral y) t)
   
   [HAS_INTEGRAL_SPIKE_INTERIOR]  Theorem
      
      ⊢ ∀f g a b y.
          (∀x. x ∈ interval (a,b) ⇒ g x = f x) ∧
          (f has_integral y) (interval [(a,b)]) ⇒
          (g has_integral y) (interval [(a,b)])
   
   [HAS_INTEGRAL_SPIKE_INTERIOR_EQ]  Theorem
      
      ⊢ ∀f g a b y.
          (∀x. x ∈ interval (a,b) ⇒ g x = f x) ⇒
          ((f has_integral y) (interval [(a,b)]) ⇔
           (g has_integral y) (interval [(a,b)]))
   
   [HAS_INTEGRAL_SPIKE_SET]  Theorem
      
      ⊢ ∀f s t y.
          negligible (s DIFF t ∪ (t DIFF s)) ∧ (f has_integral y) s ⇒
          (f has_integral y) t
   
   [HAS_INTEGRAL_SPIKE_SET_EQ]  Theorem
      
      ⊢ ∀f s t y.
          negligible (s DIFF t ∪ (t DIFF s)) ⇒
          ((f has_integral y) s ⇔ (f has_integral y) t)
   
   [HAS_INTEGRAL_SPLIT]  Theorem
      
      ⊢ ∀f a b c.
          (f has_integral i) (interval [(a,b)] ∩ {x | x ≤ c}) ∧
          (f has_integral j) (interval [(a,b)] ∩ {x | x ≥ c}) ⇒
          (f has_integral i + j) (interval [(a,b)])
   
   [HAS_INTEGRAL_STRADDLE_NULL]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ∧ (g has_integral 0) s ⇒
          (f has_integral 0) s
   
   [HAS_INTEGRAL_STRETCH]  Theorem
      
      ⊢ ∀f i m a b.
          (f has_integral i) (interval [(a,b)]) ∧ m 1 ≠ 0 ⇒
          ((λx. f (m 1 * x)) has_integral (abs (product (1 .. 1) m))⁻¹ * i)
            (IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)]))
   
   [HAS_INTEGRAL_SUB]  Theorem
      
      ⊢ ∀f g s k l.
          (f has_integral k) s ∧ (g has_integral l) s ⇒
          ((λx. f x − g x) has_integral k − l) s
   
   [HAS_INTEGRAL_SUBSET_COMPONENT_LE]  Theorem
      
      ⊢ ∀f s t i j.
          s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
          (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_SUBSET_DROP_LE]  Theorem
      
      ⊢ ∀f s t i j.
          s ⊆ t ∧ (f has_integral i) s ∧ (f has_integral j) t ∧
          (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
          i ≤ j
   
   [HAS_INTEGRAL_SUM]  Theorem
      
      ⊢ ∀f s t.
          FINITE t ∧ (∀a. a ∈ t ⇒ (f a has_integral i a) s) ⇒
          ((λx. sum t (λa. f a x)) has_integral sum t i) s
   
   [HAS_INTEGRAL_TWIDDLE]  Theorem
      
      ⊢ ∀f g h r i a b.
          0 < r ∧ (∀x. h (g x) = x) ∧ (∀x. g (h x) = x) ∧
          (∀x. g continuous at x) ∧
          (∀u v. ∃w z. IMAGE g (interval [(u,v)]) = interval [(w,z)]) ∧
          (∀u v. ∃w z. IMAGE h (interval [(u,v)]) = interval [(w,z)]) ∧
          (∀u v.
             content (IMAGE g (interval [(u,v)])) =
             r * content (interval [(u,v)])) ∧
          (f has_integral i) (interval [(a,b)]) ⇒
          ((λx. f (g x)) has_integral r⁻¹ * i) (IMAGE h (interval [(a,b)]))
   
   [HAS_INTEGRAL_UNION]  Theorem
      
      ⊢ ∀f i j s t.
          (f has_integral i) s ∧ (f has_integral j) t ∧ negligible (s ∩ t) ⇒
          (f has_integral i + j) (s ∪ t)
   
   [HAS_INTEGRAL_UNIQUE]  Theorem
      
      ⊢ ∀f i k1 k2. (f has_integral k1) i ∧ (f has_integral k2) i ⇒ k1 = k2
   
   [HENSTOCK_LEMMA]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀p. p tagged_partial_division_of interval [(a,b)] ∧
                      d FINE p ⇒
                      sum p (λ(x,k). abs (content k * f x − integral k f)) <
                      e
   
   [HENSTOCK_LEMMA_PART1]  Theorem
      
      ⊢ ∀f a b d e.
          f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
          (∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
               abs
                 (sum p (λ(x,k). content k * f x) −
                  integral (interval [(a,b)]) f) < e) ⇒
          ∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
              abs (sum p (λ(x,k). content k * f x − integral k f)) ≤ e
   
   [HENSTOCK_LEMMA_PART2]  Theorem
      
      ⊢ ∀f a b d e.
          f integrable_on interval [(a,b)] ∧ 0 < e ∧ gauge d ∧
          (∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
               abs
                 (sum p (λ(x,k). content k * f x) −
                  integral (interval [(a,b)]) f) < e) ⇒
          ∀p. p tagged_partial_division_of interval [(a,b)] ∧ d FINE p ⇒
              sum p (λ(x,k). abs (content k * f x − integral k f)) ≤
              2 * 1 * e
   
   [INCREASING_BOUNDED_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ⇒
          f has_bounded_variation_on interval [(a,b)]
   
   [INCREASING_BOUNDED_VARIATION_GEN]  Theorem
      
      ⊢ ∀f s.
          bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f x ≤ f y) ⇒
          f has_bounded_variation_on s
   
   [INCREASING_LEFT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ∧ c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(a,c)])
   
   [INCREASING_RIGHT_LIMIT]  Theorem
      
      ⊢ ∀f a b c.
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ∧ c ∈ interval [(a,b)] ⇒
          ∃l. (f ⟶ l) (at c within interval [(c,b)])
   
   [INCREASING_VECTOR_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          interval [(a,b)] ≠ ∅ ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ⇒
          vector_variation (interval [(a,b)]) f = f b − f a
   
   [INDEFINITE_INTEGRAL_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b c d e.
          f integrable_on interval [(a,b)] ∧ c ∈ interval [(a,b)] ∧
          d ∈ interval [(a,b)] ∧ 0 < e ⇒
          ∃k. 0 < k ∧
              ∀c' d'.
                c' ∈ interval [(a,b)] ∧ d' ∈ interval [(a,b)] ∧
                abs (c' − c) ≤ k ∧ abs (d' − d) ≤ k ⇒
                abs
                  (integral (interval [(c',d')]) f −
                   integral (interval [(c,d)]) f) < e
   
   [INDEFINITE_INTEGRAL_CONTINUOUS_LEFT]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          (λx. integral (interval [(x,b)]) f) continuous_on
          interval [(a,b)]
   
   [INDEFINITE_INTEGRAL_CONTINUOUS_RIGHT]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          (λx. integral (interval [(a,x)]) f) continuous_on
          interval [(a,b)]
   
   [INDICATOR_EMPTY]  Theorem
      
      ⊢ indicator ∅ = (λx. 0)
   
   [INTEGRABLE_0]  Theorem
      
      ⊢ ∀s. (λx. 0) integrable_on s
   
   [INTEGRABLE_ADD]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ⇒
          (λx. f x + g x) integrable_on s
   
   [INTEGRABLE_AFFINITY]  Theorem
      
      ⊢ ∀f a b m c.
          f integrable_on interval [(a,b)] ∧ m ≠ 0 ⇒
          (λx. f (m * x + c)) integrable_on
          IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) (interval [(a,b)])
   
   [INTEGRABLE_ALT]  Theorem
      
      ⊢ ∀f s.
          f integrable_on s ⇔
          (∀a b.
             (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
          ∀e. 0 < e ⇒
              ∃B. 0 < B ∧
                  ∀a b c d.
                    ball (0,B) ⊆ interval [(a,b)] ∧
                    ball (0,B) ⊆ interval [(c,d)] ⇒
                    abs
                      (integral (interval [(a,b)])
                         (λx. if x ∈ s then f x else 0) −
                       integral (interval [(c,d)])
                         (λx. if x ∈ s then f x else 0)) < e
   
   [INTEGRABLE_ALT_SUBSET]  Theorem
      
      ⊢ ∀f s.
          f integrable_on s ⇔
          (∀a b.
             (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
          ∀e. 0 < e ⇒
              ∃B. 0 < B ∧
                  ∀a b c d.
                    ball (0,B) ⊆ interval [(a,b)] ∧
                    interval [(a,b)] ⊆ interval [(c,d)] ⇒
                    abs
                      (integral (interval [(a,b)])
                         (λx. if x ∈ s then f x else 0) −
                       integral (interval [(c,d)])
                         (λx. if x ∈ s then f x else 0)) < e
   
   [INTEGRABLE_BOUNDED_VARIATION]  Theorem
      
      ⊢ ∀f a b.
          f has_bounded_variation_on interval [(a,b)] ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_BOUNDED_VARIATION_BILINEAR_LMUL]  Theorem
      
      ⊢ ∀op f g a b.
          bilinear op ∧ f integrable_on interval [(a,b)] ∧
          g has_bounded_variation_on interval [(a,b)] ⇒
          (λx. op (g x) (f x)) integrable_on interval [(a,b)]
   
   [INTEGRABLE_BOUNDED_VARIATION_BILINEAR_RMUL]  Theorem
      
      ⊢ ∀op f g a b.
          bilinear op ∧ f integrable_on interval [(a,b)] ∧
          g has_bounded_variation_on interval [(a,b)] ⇒
          (λx. op (f x) (g x)) integrable_on interval [(a,b)]
   
   [INTEGRABLE_BOUNDED_VARIATION_PRODUCT]  Theorem
      
      ⊢ ∀f g a b.
          f integrable_on interval [(a,b)] ∧
          g has_bounded_variation_on interval [(a,b)] ⇒
          (λx. g x * f x) integrable_on interval [(a,b)]
   
   [INTEGRABLE_BOUNDED_VARIATION_PRODUCT_ALT]  Theorem
      
      ⊢ ∀f g a b.
          f integrable_on interval [(a,b)] ∧
          g has_bounded_variation_on interval [(a,b)] ⇒
          (λx. g x * f x) integrable_on interval [(a,b)]
   
   [INTEGRABLE_BY_PARTS]  Theorem
      
      ⊢ ∀bop f g f' g' a b c.
          bilinear bop ∧ COUNTABLE c ∧
          (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) DIFF c ⇒
               (f has_vector_derivative f' x) (at x) ∧
               (g has_vector_derivative g' x) (at x)) ∧
          (λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇒
          (λx. bop (f' x) (g x)) integrable_on interval [(a,b)]
   
   [INTEGRABLE_BY_PARTS_EQ]  Theorem
      
      ⊢ ∀bop f g f' g' a b c.
          bilinear bop ∧ COUNTABLE c ∧
          (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) DIFF c ⇒
               (f has_vector_derivative f' x) (at x) ∧
               (g has_vector_derivative g' x) (at x)) ⇒
          ((λx. bop (f x) (g' x)) integrable_on interval [(a,b)] ⇔
           (λx. bop (f' x) (g x)) integrable_on interval [(a,b)])
   
   [INTEGRABLE_CASES]  Theorem
      
      ⊢ ∀P f g s.
          f integrable_on {x | x ∈ s ∧ P x} ∧
          g integrable_on {x | x ∈ s ∧ ¬P x} ⇒
          (λx. if P x then f x else g x) integrable_on s
   
   [INTEGRABLE_CAUCHY]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇔
          ∀e. 0 < e ⇒
              ∃d. gauge d ∧
                  ∀p1 p2.
                    p1 tagged_division_of interval [(a,b)] ∧ d FINE p1 ∧
                    p2 tagged_division_of interval [(a,b)] ∧ d FINE p2 ⇒
                    abs
                      (sum p1 (λ(x,k). content k * f x) −
                       sum p2 (λ(x,k). content k * f x)) < e
   
   [INTEGRABLE_CMUL]  Theorem
      
      ⊢ ∀f c s. f integrable_on s ⇒ (λx. c * f x) integrable_on s
   
   [INTEGRABLE_CMUL_EQ]  Theorem
      
      ⊢ ∀f s c. (λx. c * f x) integrable_on s ⇔ c = 0 ∨ f integrable_on s
   
   [INTEGRABLE_COMBINE]  Theorem
      
      ⊢ ∀f a b c.
          a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,c)] ∧
          f integrable_on interval [(c,b)] ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_COMBINE_DIVISION]  Theorem
      
      ⊢ ∀f d s.
          d division_of s ∧ (∀i. i ∈ d ⇒ f integrable_on i) ⇒
          f integrable_on s
   
   [INTEGRABLE_COMPONENTWISE]  Theorem
      
      ⊢ ∀f s. f integrable_on s ⇔ (λx. f x) integrable_on s
   
   [INTEGRABLE_CONST]  Theorem
      
      ⊢ ∀a b c. (λx. c) integrable_on interval [(a,b)]
   
   [INTEGRABLE_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b.
          f continuous_on interval [(a,b)] ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_DECREASING]  Theorem
      
      ⊢ ∀f a b.
          (∀x y i.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f y ≤ f x) ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_DECREASING_PRODUCT]  Theorem
      
      ⊢ ∀f g a b.
          f integrable_on interval [(a,b)] ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g y ≤ g x) ⇒
          (λx. g x * f x) integrable_on interval [(a,b)]
   
   [INTEGRABLE_DECREASING_PRODUCT_UNIV]  Theorem
      
      ⊢ ∀f g B.
          f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g y ≤ g x) ∧
          (∀x. abs (g x) ≤ B) ⇒
          (λx. g x * f x) integrable_on 𝕌(:real)
   
   [INTEGRABLE_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x = g x) ∧ f integrable_on s ⇒ g integrable_on s
   
   [INTEGRABLE_INCREASING]  Theorem
      
      ⊢ ∀f a b.
          (∀x y i.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             f x ≤ f y) ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_INCREASING_PRODUCT]  Theorem
      
      ⊢ ∀f g a b.
          f integrable_on interval [(a,b)] ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          (λx. g x * f x) integrable_on interval [(a,b)]
   
   [INTEGRABLE_INCREASING_PRODUCT_UNIV]  Theorem
      
      ⊢ ∀f g B.
          f integrable_on 𝕌(:real) ∧ (∀x y. x ≤ y ⇒ g x ≤ g y) ∧
          (∀x. abs (g x) ≤ B) ⇒
          (λx. g x * f x) integrable_on 𝕌(:real)
   
   [INTEGRABLE_INTEGRAL]  Theorem
      
      ⊢ ∀f i. f integrable_on i ⇒ (f has_integral integral i f) i
   
   [INTEGRABLE_LINEAR]  Theorem
      
      ⊢ ∀f h s. f integrable_on s ∧ linear h ⇒ h ∘ f integrable_on s
   
   [INTEGRABLE_MIN_CONST]  Theorem
      
      ⊢ ∀f s t.
          0 ≤ t ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (λx. f x) integrable_on s ⇒
          (λx. min (f x) t) integrable_on s
   
   [INTEGRABLE_NEG]  Theorem
      
      ⊢ ∀f s. f integrable_on s ⇒ (λx. -f x) integrable_on s
   
   [INTEGRABLE_ON_ALL_INTERVALS_INTEGRABLE_BOUND]  Theorem
      
      ⊢ ∀f g s.
          (∀a b.
             (λx. if x ∈ s then f x else 0) integrable_on interval [(a,b)]) ∧
          (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ g integrable_on s ⇒
          f integrable_on s
   
   [INTEGRABLE_ON_EMPTY]  Theorem
      
      ⊢ ∀f. f integrable_on ∅
   
   [INTEGRABLE_ON_LITTLE_SUBINTERVALS]  Theorem
      
      ⊢ ∀f a b.
          (∀x. x ∈ interval [(a,b)] ⇒
               ∃d. 0 < d ∧
                   ∀u v.
                     x ∈ interval [(u,v)] ∧ interval [(u,v)] ⊆ ball (x,d) ∧
                     interval [(u,v)] ⊆ interval [(a,b)] ⇒
                     f integrable_on interval [(u,v)]) ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_ON_NULL]  Theorem
      
      ⊢ ∀f a b.
          content (interval [(a,b)]) = 0 ⇒ f integrable_on interval [(a,b)]
   
   [INTEGRABLE_ON_REFL]  Theorem
      
      ⊢ ∀f a. f integrable_on interval [(a,a)]
   
   [INTEGRABLE_ON_SUBDIVISION]  Theorem
      
      ⊢ ∀f s d i.
          d division_of i ∧ f integrable_on s ∧ i ⊆ s ⇒ f integrable_on i
   
   [INTEGRABLE_ON_SUBINTERVAL]  Theorem
      
      ⊢ ∀f s a b.
          f integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_ON_SUPERSET]  Theorem
      
      ⊢ ∀f s t.
          (∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ f integrable_on s ⇒
          f integrable_on t
   
   [INTEGRABLE_REFLECT]  Theorem
      
      ⊢ ∀f a b.
          (λx. f (-x)) integrable_on interval [(-b,-a)] ⇔
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_REFLECT_GEN]  Theorem
      
      ⊢ ∀f s.
          (λx. f (-x)) integrable_on s ⇔ f integrable_on IMAGE (λx. -x) s
   
   [INTEGRABLE_RESTRICT]  Theorem
      
      ⊢ ∀f s t.
          s ⊆ t ⇒
          ((λx. if x ∈ s then f x else 0) integrable_on t ⇔
           f integrable_on s)
   
   [INTEGRABLE_RESTRICT_INTER]  Theorem
      
      ⊢ ∀f s t.
          (λx. if x ∈ s then f x else 0) integrable_on t ⇔
          f integrable_on s ∩ t
   
   [INTEGRABLE_RESTRICT_UNIV]  Theorem
      
      ⊢ ∀f s.
          (λx. if x ∈ s then f x else 0) integrable_on 𝕌(:real) ⇔
          f integrable_on s
   
   [INTEGRABLE_SPIKE]  Theorem
      
      ⊢ ∀f g s t.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          f integrable_on t ⇒
          g integrable_on t
   
   [INTEGRABLE_SPIKE_EQ]  Theorem
      
      ⊢ ∀f g s t.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          (f integrable_on t ⇔ g integrable_on t)
   
   [INTEGRABLE_SPIKE_FINITE]  Theorem
      
      ⊢ ∀f g s.
          FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          f integrable_on t ⇒
          g integrable_on t
   
   [INTEGRABLE_SPIKE_INTERIOR]  Theorem
      
      ⊢ ∀f g a b.
          (∀x. x ∈ interval (a,b) ⇒ g x = f x) ⇒
          f integrable_on interval [(a,b)] ⇒
          g integrable_on interval [(a,b)]
   
   [INTEGRABLE_SPIKE_SET]  Theorem
      
      ⊢ ∀f s t.
          negligible (s DIFF t ∪ (t DIFF s)) ⇒
          f integrable_on s ⇒
          f integrable_on t
   
   [INTEGRABLE_SPIKE_SET_EQ]  Theorem
      
      ⊢ ∀f s t.
          negligible (s DIFF t ∪ (t DIFF s)) ⇒
          (f integrable_on s ⇔ f integrable_on t)
   
   [INTEGRABLE_SPLIT]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ⇒
          f integrable_on interval [(a,b)] ∩ {x | x ≤ c} ∧
          f integrable_on interval [(a,b)] ∩ {x | x ≥ c}
   
   [INTEGRABLE_STRADDLE]  Theorem
      
      ⊢ ∀f s.
          (∀e. 0 < e ⇒
               ∃g h i j.
                 (g has_integral i) s ∧ (h has_integral j) s ∧
                 abs (i − j) < e ∧ ∀x. x ∈ s ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
          f integrable_on s
   
   [INTEGRABLE_STRADDLE_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          (∀e. 0 < e ⇒
               ∃g h i j.
                 (g has_integral i) (interval [(a,b)]) ∧
                 (h has_integral j) (interval [(a,b)]) ∧ abs (i − j) < e ∧
                 ∀x. x ∈ interval [(a,b)] ⇒ g x ≤ f x ∧ f x ≤ h x) ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRABLE_STRETCH]  Theorem
      
      ⊢ ∀f m a b.
          f integrable_on interval [(a,b)] ∧ m 1 ≠ 0 ⇒
          (λx. f (m 1 * x)) integrable_on
          IMAGE (λx. (m 1)⁻¹ * x) (interval [(a,b)])
   
   [INTEGRABLE_SUB]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ⇒
          (λx. f x − g x) integrable_on s
   
   [INTEGRABLE_SUBINTERVAL]  Theorem
      
      ⊢ ∀f a b c d.
          f integrable_on interval [(a,b)] ∧
          interval [(c,d)] ⊆ interval [(a,b)] ⇒
          f integrable_on interval [(c,d)]
   
   [INTEGRABLE_SUM]  Theorem
      
      ⊢ ∀f s t.
          FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
          (λx. sum t (λa. f a x)) integrable_on s
   
   [INTEGRABLE_UNIFORM_LIMIT]  Theorem
      
      ⊢ ∀f a b.
          (∀e. 0 < e ⇒
               ∃g. (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ∧
                   g integrable_on interval [(a,b)]) ⇒
          f integrable_on interval [(a,b)]
   
   [INTEGRAL_0]  Theorem
      
      ⊢ ∀s. integral s (λx. 0) = 0
   
   [INTEGRAL_ABS_BOUND_INTEGRAL]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ∧
          (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
          abs (integral s f) ≤ integral s g
   
   [INTEGRAL_ABS_BOUND_INTEGRAL_AE]  Theorem
      
      ⊢ ∀f g s t.
          f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
          (∀x. x ∈ s DIFF t ⇒ abs (f x) ≤ g x) ⇒
          abs (integral s f) ≤ integral s g
   
   [INTEGRAL_ABS_BOUND_INTEGRAL_COMPONENT]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ∧
          (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
          abs (integral s f) ≤ integral s g
   
   [INTEGRAL_ADD]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ⇒
          integral s (λx. f x + g x) = integral s f + integral s g
   
   [INTEGRAL_CMUL]  Theorem
      
      ⊢ ∀f c s.
          f integrable_on s ⇒ integral s (λx. c * f x) = c * integral s f
   
   [INTEGRAL_COMBINE]  Theorem
      
      ⊢ ∀f a b c.
          a ≤ c ∧ c ≤ b ∧ f integrable_on interval [(a,b)] ⇒
          integral (interval [(a,c)]) f + integral (interval [(c,b)]) f =
          integral (interval [(a,b)]) f
   
   [INTEGRAL_COMBINE_DIVISION_BOTTOMUP]  Theorem
      
      ⊢ ∀f d s.
          d division_of s ∧ (∀k. k ∈ d ⇒ f integrable_on k) ⇒
          integral s f = sum d (λi. integral i f)
   
   [INTEGRAL_COMBINE_DIVISION_TOPDOWN]  Theorem
      
      ⊢ ∀f d s.
          f integrable_on s ∧ d division_of s ⇒
          integral s f = sum d (λi. integral i f)
   
   [INTEGRAL_COMBINE_TAGGED_DIVISION_BOTTOMUP]  Theorem
      
      ⊢ ∀f p a b.
          p tagged_division_of interval [(a,b)] ∧
          (∀x k. (x,k) ∈ p ⇒ f integrable_on k) ⇒
          integral (interval [(a,b)]) f = sum p (λ(x,k). integral k f)
   
   [INTEGRAL_COMBINE_TAGGED_DIVISION_TOPDOWN]  Theorem
      
      ⊢ ∀f a b p.
          f integrable_on interval [(a,b)] ∧
          p tagged_division_of interval [(a,b)] ⇒
          integral (interval [(a,b)]) f = sum p (λ(x,k). integral k f)
   
   [INTEGRAL_COMPONENT]  Theorem
      
      ⊢ ∀f s. f integrable_on s ⇒ integral s f = integral s (λx. f x)
   
   [INTEGRAL_COMPONENT_LBOUND]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ B ≤ f x) ⇒
          B * content (interval [(a,b)]) ≤ integral (interval [(a,b)]) f
   
   [INTEGRAL_COMPONENT_LE]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
          integral s f ≤ integral s g
   
   [INTEGRAL_COMPONENT_LE_AE]  Theorem
      
      ⊢ ∀f g s k t.
          negligible t ∧ f integrable_on s ∧ g integrable_on s ∧
          (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
          integral s f ≤ integral s g
   
   [INTEGRAL_COMPONENT_POS]  Theorem
      
      ⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f
   
   [INTEGRAL_COMPONENT_UBOUND]  Theorem
      
      ⊢ ∀f a b.
          f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ B) ⇒
          integral (interval [(a,b)]) f ≤ B * content (interval [(a,b)])
   
   [INTEGRAL_CONST]  Theorem
      
      ⊢ ∀a b c.
          integral (interval [(a,b)]) (λx. c) =
          content (interval [(a,b)]) * c
   
   [INTEGRAL_DIFF]  Theorem
      
      ⊢ ∀f s t.
          f integrable_on s ∧ f integrable_on t ∧ negligible (t DIFF s) ⇒
          integral (s DIFF t) f = integral s f − integral t f
   
   [INTEGRAL_DROP_LE]  Theorem
      
      ⊢ ∀f g s.
          f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
          integral s f ≤ integral s g
   
   [INTEGRAL_DROP_POS]  Theorem
      
      ⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f
   
   [INTEGRAL_DROP_POS_AE]  Theorem
      
      ⊢ ∀f s t.
          f integrable_on s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
          0 ≤ integral s f
   
   [INTEGRAL_EMPTY]  Theorem
      
      ⊢ ∀f. integral ∅ f = 0
   
   [INTEGRAL_EQ]  Theorem
      
      ⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ integral s f = integral s g
   
   [INTEGRAL_EQ_0]  Theorem
      
      ⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ integral s f = 0
   
   [INTEGRAL_EQ_HAS_INTEGRAL]  Theorem
      
      ⊢ ∀s f y.
          f integrable_on s ⇒ (integral s f = y ⇔ (f has_integral y) s)
   
   [INTEGRAL_HAS_VECTOR_DERIVATIVE]  Theorem
      
      ⊢ ∀f a b.
          f continuous_on interval [(a,b)] ⇒
          ∀x. x ∈ interval [(a,b)] ⇒
              ((λu. integral (interval [(a,u)]) f) has_vector_derivative
               f x) (at x within interval [(a,b)])
   
   [INTEGRAL_HAS_VECTOR_DERIVATIVE_POINTWISE]  Theorem
      
      ⊢ ∀f a b x.
          f integrable_on interval [(a,b)] ∧ x ∈ interval [(a,b)] ∧
          f continuous (at x within interval [(a,b)]) ⇒
          ((λu. integral (interval [(a,u)]) f) has_vector_derivative f x)
            (at x within interval [(a,b)])
   
   [INTEGRAL_LE_AE]  Theorem
      
      ⊢ ∀f g s t.
          f integrable_on s ∧ g integrable_on s ∧ negligible t ∧
          (∀x. x ∈ s DIFF t ⇒ f x ≤ g x) ⇒
          integral s f ≤ integral s g
   
   [INTEGRAL_LINEAR]  Theorem
      
      ⊢ ∀f s h.
          f integrable_on s ∧ linear h ⇒
          integral s (h ∘ f) = h (integral s f)
   
   [INTEGRAL_NEG]  Theorem
      
      ⊢ ∀f s. f integrable_on s ⇒ integral s (λx. -f x) = -integral s f
   
   [INTEGRAL_NULL]  Theorem
      
      ⊢ ∀f a b.
          content (interval [(a,b)]) = 0 ⇒
          integral (interval [(a,b)]) f = 0
   
   [INTEGRAL_REFL]  Theorem
      
      ⊢ ∀f a. integral (interval [(a,a)]) f = 0
   
   [INTEGRAL_REFLECT]  Theorem
      
      ⊢ ∀f a b.
          integral (interval [(-b,-a)]) (λx. f (-x)) =
          integral (interval [(a,b)]) f
   
   [INTEGRAL_REFLECT_GEN]  Theorem
      
      ⊢ ∀f s. integral s (λx. f (-x)) = integral (IMAGE (λx. -x) s) f
   
   [INTEGRAL_RESTRICT]  Theorem
      
      ⊢ ∀f s t.
          s ⊆ t ⇒ integral t (λx. if x ∈ s then f x else 0) = integral s f
   
   [INTEGRAL_RESTRICT_INTER]  Theorem
      
      ⊢ ∀f s t.
          integral t (λx. if x ∈ s then f x else 0) = integral (s ∩ t) f
   
   [INTEGRAL_RESTRICT_UNIV]  Theorem
      
      ⊢ ∀f s.
          integral 𝕌(:real) (λx. if x ∈ s then f x else 0) = integral s f
   
   [INTEGRAL_SPIKE]  Theorem
      
      ⊢ ∀f g s t y.
          negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
          integral t f = integral t g
   
   [INTEGRAL_SPIKE_SET]  Theorem
      
      ⊢ ∀f s t.
          negligible (s DIFF t ∪ (t DIFF s)) ⇒ integral s f = integral t f
   
   [INTEGRAL_SPLIT]  Theorem
      
      ⊢ ∀f a b t.
          f integrable_on interval [(a,b)] ⇒
          integral (interval [(a,b)]) f =
          integral (interval [(a,@f. f = min b t)]) f +
          integral (interval [((@f. f = max a t),b)]) f
   
   [INTEGRAL_SPLIT_SIGNED]  Theorem
      
      ⊢ ∀f a b t.
          a ≤ t ∧ a ≤ b ∧ f integrable_on interval [(a,@f. f = max b t)] ⇒
          integral (interval [(a,b)]) f =
          integral (interval [(a,@f. f = t)]) f +
          (if b < t then -1 else 1) *
          integral (interval [((@f. f = min b t),@f. f = max b t)]) f
   
   [INTEGRAL_SUB]  Theorem
      
      ⊢ ∀f g k l s.
          f integrable_on s ∧ g integrable_on s ⇒
          integral s (λx. f x − g x) = integral s f − integral s g
   
   [INTEGRAL_SUBSET_COMPONENT_LE]  Theorem
      
      ⊢ ∀f s t.
          s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧
          (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
          integral s f ≤ integral t f
   
   [INTEGRAL_SUBSET_DROP_LE]  Theorem
      
      ⊢ ∀f s t.
          s ⊆ t ∧ f integrable_on s ∧ f integrable_on t ∧
          (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
          integral s f ≤ integral t f
   
   [INTEGRAL_SUM]  Theorem
      
      ⊢ ∀f s t.
          FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
          integral s (λx. sum t (λa. f a x)) = sum t (λa. integral s (f a))
   
   [INTEGRAL_UNION]  Theorem
      
      ⊢ ∀f s t.
          f integrable_on s ∧ f integrable_on t ∧ negligible (s ∩ t) ⇒
          integral (s ∪ t) f = integral s f + integral t f
   
   [INTEGRAL_UNIQUE]  Theorem
      
      ⊢ ∀f y k. (f has_integral y) k ⇒ integral k f = y
   
   [INTEGRATION_BY_PARTS]  Theorem
      
      ⊢ ∀bop f g f' g' a b c y.
          bilinear bop ∧ a ≤ b ∧ COUNTABLE c ∧
          (λx. bop (f x) (g x)) continuous_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) DIFF c ⇒
               (f has_vector_derivative f' x) (at x) ∧
               (g has_vector_derivative g' x) (at x)) ∧
          ((λx. bop (f x) (g' x)) has_integral
           bop (f b) (g b) − bop (f a) (g a) − y) (interval [(a,b)]) ⇒
          ((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])
   
   [INTEGRATION_BY_PARTS_SIMPLE]  Theorem
      
      ⊢ ∀bop f g f' g' a b y.
          bilinear bop ∧ a ≤ b ∧
          (∀x. x ∈ interval [(a,b)] ⇒
               (f has_vector_derivative f' x)
                 (at x within interval [(a,b)]) ∧
               (g has_vector_derivative g' x)
                 (at x within interval [(a,b)])) ∧
          ((λx. bop (f x) (g' x)) has_integral
           bop (f b) (g b) − bop (f a) (g a) − y) (interval [(a,b)]) ⇒
          ((λx. bop (f' x) (g x)) has_integral y) (interval [(a,b)])
   
   [INTERIOR_SUBSET_UNION_INTERVALS]  Theorem
      
      ⊢ ∀s i j.
          (∃a b. i = interval [(a,b)]) ∧ (∃c d. j = interval [(c,d)]) ∧
          interior j ≠ ∅ ∧ i ⊆ j ∪ s ∧ interior i ∩ interior j = ∅ ⇒
          interior i ⊆ interior s
   
   [INTERVAL_BISECTION]  Theorem
      
      ⊢ ∀P. P ∅ ∧
            (∀s t. P s ∧ P t ∧ interior s ∩ interior t = ∅ ⇒ P (s ∪ t)) ⇒
            ∀a b.
              ¬P (interval [(a,b)]) ⇒
              ∃x. x ∈ interval [(a,b)] ∧
                  ∀e. 0 < e ⇒
                      ∃c d.
                        x ∈ interval [(c,d)] ∧
                        interval [(c,d)] ⊆ ball (x,e) ∧
                        interval [(c,d)] ⊆ interval [(a,b)] ∧
                        ¬P (interval [(c,d)])
   
   [INTERVAL_BISECTION_STEP]  Theorem
      
      ⊢ ∀P. P ∅ ∧
            (∀s t. P s ∧ P t ∧ interior s ∩ interior t = ∅ ⇒ P (s ∪ t)) ⇒
            ∀a b.
              ¬P (interval [(a,b)]) ⇒
              ∃c d.
                ¬P (interval [(c,d)]) ∧ a ≤ c ∧ c ≤ d ∧ d ≤ b ∧
                2 * (d − c) ≤ b − a
   
   [INTERVAL_BOUNDS_EMPTY]  Theorem
      
      ⊢ interval_upperbound ∅ = interval_lowerbound ∅
   
   [INTERVAL_BOUNDS_NULL]  Theorem
      
      ⊢ ∀a b.
          content (interval [(a,b)]) = 0 ⇒
          interval_upperbound (interval [(a,b)]) =
          interval_lowerbound (interval [(a,b)])
   
   [INTERVAL_DOUBLESPLIT]  Theorem
      
      ⊢ ∀e a b c.
          interval [(a,b)] ∩ {x | abs (x − c) ≤ e} =
          interval [(max a (c − e),min b (c + e))]
   
   [INTERVAL_IMAGE_AFFINITY_INTERVAL]  Theorem
      
      ⊢ ∀a b m c. ∃u v.
          IMAGE (λx. m * x + c) (interval [(a,b)]) = interval [(u,v)]
   
   [INTERVAL_LOWERBOUND]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ interval_lowerbound (interval [(a,b)]) = a
   
   [INTERVAL_LOWERBOUND_NONEMPTY]  Theorem
      
      ⊢ ∀a b.
          interval [(a,b)] ≠ ∅ ⇒ interval_lowerbound (interval [(a,b)]) = a
   
   [INTERVAL_SPLIT]  Theorem
      
      ⊢ ∀a b c.
          interval [(a,b)] ∩ {x | x ≤ c} = interval [(a,min b c)] ∧
          interval [(a,b)] ∩ {x | x ≥ c} = interval [(max a c,b)]
   
   [INTERVAL_SUBDIVISION]  Theorem
      
      ⊢ ∀a b c.
          c ∈ interval [(a,b)] ⇒
          IMAGE
            (λs.
                 interval
                   [((@f. f = if 1 ∈ s then c else a),
                     @f. f = if 1 ∈ s then b else c)]) {s | s ⊆ 1 .. 1} division_of
          interval [(a,b)]
   
   [INTERVAL_UPPERBOUND]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ interval_upperbound (interval [(a,b)]) = b
   
   [INTERVAL_UPPERBOUND_NONEMPTY]  Theorem
      
      ⊢ ∀a b.
          interval [(a,b)] ≠ ∅ ⇒ interval_upperbound (interval [(a,b)]) = b
   
   [INTER_INTERIOR_BIGUNION_INTERVALS]  Theorem
      
      ⊢ ∀s f.
          FINITE f ∧ open s ∧ (∀t. t ∈ f ⇒ ∃a b. t = interval [(a,b)]) ∧
          (∀t. t ∈ f ⇒ s ∩ interior t = ∅) ⇒
          s ∩ interior (BIGUNION f) = ∅
   
   [ITERATE_AND]  Theorem
      
      ⊢ ∀p s. FINITE s ⇒ (iterate $/\ s p ⇔ ∀x. x ∈ s ⇒ p x)
   
   [ITERATE_NONZERO_IMAGE_LEMMA]  Theorem
      
      ⊢ ∀op s f g a.
          monoidal op ∧ FINITE s ∧ g a = neutral op ∧
          (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ∧ x ≠ y ⇒ g (f x) = neutral op) ⇒
          iterate op {f x | x | x ∈ s ∧ f x ≠ a} g = iterate op s (g ∘ f)
   
   [ITERATE_SOME]  Theorem
      
      ⊢ ∀op.
          monoidal op ⇒
          ∀f s.
            FINITE s ⇒
            iterate (lifted op) s (λx. SOME (f x)) = SOME (iterate op s f)
   
   [MONOIDAL_AND]  Theorem
      
      ⊢ monoidal $/\
   
   [MONOIDAL_LIFTED]  Theorem
      
      ⊢ ∀op. monoidal op ⇒ monoidal (lifted op)
   
   [MONOTONE_CONVERGENCE_DECREASING]  Theorem
      
      ⊢ ∀f g s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f (SUC k) x ≤ f k x) ∧
          (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [MONOTONE_CONVERGENCE_DECREASING_AE]  Theorem
      
      ⊢ ∀f g s t.
          (∀k. f k integrable_on s) ∧ negligible t ∧
          (∀k x. x ∈ s DIFF t ⇒ f (SUC k) x ≤ f k x) ∧
          (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [MONOTONE_CONVERGENCE_INCREASING]  Theorem
      
      ⊢ ∀f g s.
          (∀k. f k integrable_on s) ∧ (∀k x. x ∈ s ⇒ f k x ≤ f (SUC k) x) ∧
          (∀x. x ∈ s ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [MONOTONE_CONVERGENCE_INCREASING_AE]  Theorem
      
      ⊢ ∀f g s t.
          (∀k. f k integrable_on s) ∧ negligible t ∧
          (∀k x. x ∈ s DIFF t ⇒ f k x ≤ f (SUC k) x) ∧
          (∀x. x ∈ s DIFF t ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
          bounded {integral s (f k) | k ∈ 𝕌(:num)} ⇒
          g integrable_on s ∧
          ((λk. integral s (f k)) ⟶ integral s g) sequentially
   
   [MONOTONE_CONVERGENCE_INTERVAL]  Theorem
      
      ⊢ ∀f g a b.
          (∀k. f k integrable_on interval [(a,b)]) ∧
          (∀k x. x ∈ interval [(a,b)] ⇒ f k x ≤ f (SUC k) x) ∧
          (∀x. x ∈ interval [(a,b)] ⇒ ((λk. f k x) ⟶ g x) sequentially) ∧
          bounded {integral (interval [(a,b)]) (f k) | k ∈ 𝕌(:num)} ⇒
          g integrable_on interval [(a,b)] ∧
          ((λk. integral (interval [(a,b)]) (f k)) ⟶
           integral (interval [(a,b)]) g) sequentially
   
   [NEGLIGIBLE]  Theorem
      
      ⊢ ∀s. negligible s ⇔ ∀t. (indicator s has_integral 0) t
   
   [NEGLIGIBLE_BIGUNION]  Theorem
      
      ⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ negligible t) ⇒ negligible (BIGUNION s)
   
   [NEGLIGIBLE_BOUNDED_SUBSETS]  Theorem
      
      ⊢ ∀s. negligible s ⇔ ∀t. bounded t ∧ t ⊆ s ⇒ negligible t
   
   [NEGLIGIBLE_COUNTABLE]  Theorem
      
      ⊢ ∀s. COUNTABLE s ⇒ negligible s
   
   [NEGLIGIBLE_COUNTABLE_BIGUNION]  Theorem
      
      ⊢ ∀s. (∀n. negligible (s n)) ⇒
            negligible (BIGUNION {s n | n ∈ 𝕌(:num)})
   
   [NEGLIGIBLE_DIFF]  Theorem
      
      ⊢ ∀s t. negligible s ⇒ negligible (s DIFF t)
   
   [NEGLIGIBLE_EMPTY]  Theorem
      
      ⊢ negligible ∅
   
   [NEGLIGIBLE_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ negligible s
   
   [NEGLIGIBLE_FRONTIER_INTERVAL]  Theorem
      
      ⊢ ∀a b. negligible (interval [(a,b)] DIFF interval (a,b))
   
   [NEGLIGIBLE_INSERT]  Theorem
      
      ⊢ ∀a s. negligible (a INSERT s) ⇔ negligible s
   
   [NEGLIGIBLE_INTER]  Theorem
      
      ⊢ ∀s t. negligible s ∨ negligible t ⇒ negligible (s ∩ t)
   
   [NEGLIGIBLE_ON_COUNTABLE_INTERVALS]  Theorem
      
      ⊢ ∀s. negligible s ⇔ ∀n. negligible (s ∩ interval [(-n,n)])
   
   [NEGLIGIBLE_ON_INTERVALS]  Theorem
      
      ⊢ ∀s. negligible s ⇔ ∀a b. negligible (s ∩ interval [(a,b)])
   
   [NEGLIGIBLE_ON_UNIV]  Theorem
      
      ⊢ ∀s. negligible s ⇔ (indicator s has_integral 0) 𝕌(:real)
   
   [NEGLIGIBLE_SING]  Theorem
      
      ⊢ ∀a. negligible {a}
   
   [NEGLIGIBLE_STANDARD_HYPERPLANE]  Theorem
      
      ⊢ ∀c. negligible {x | x = c}
   
   [NEGLIGIBLE_SUBSET]  Theorem
      
      ⊢ ∀s t. negligible s ∧ t ⊆ s ⇒ negligible t
   
   [NEGLIGIBLE_UNION]  Theorem
      
      ⊢ ∀s t. negligible s ∧ negligible t ⇒ negligible (s ∪ t)
   
   [NEGLIGIBLE_UNION_EQ]  Theorem
      
      ⊢ ∀s t. negligible (s ∪ t) ⇔ negligible s ∧ negligible t
   
   [NEUTRAL_AND]  Theorem
      
      ⊢ neutral $/\ ⇔ T
   
   [NEUTRAL_LIFTED]  Theorem
      
      ⊢ ∀op. monoidal op ⇒ neutral (lifted op) = SOME (neutral op)
   
   [NONNEGATIVE_ABSOLUTELY_INTEGRABLE]  Theorem
      
      ⊢ ∀f s.
          (∀x i. x ∈ s ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
          f absolutely_integrable_on s
   
   [NONNEGATIVE_ABSOLUTELY_INTEGRABLE_AE]  Theorem
      
      ⊢ ∀f s t.
          negligible t ∧ (∀x i. x ∈ s DIFF t ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
          f absolutely_integrable_on s
   
   [OPEN_INTERVAL_LOWERBOUND]  Theorem
      
      ⊢ ∀a b. a < b ⇒ interval_lowerbound (interval (a,b)) = a
   
   [OPEN_INTERVAL_UPPERBOUND]  Theorem
      
      ⊢ ∀a b. a < b ⇒ interval_upperbound (interval (a,b)) = b
   
   [OPERATIVE_1_LE]  Theorem
      
      ⊢ ∀op.
          monoidal op ⇒
          ∀f. operative op f ⇔
              (∀a b. b ≤ a ⇒ f (interval [(a,b)]) = neutral op) ∧
              ∀a b c.
                a ≤ c ∧ c ≤ b ⇒
                op (f (interval [(a,c)])) (f (interval [(c,b)])) =
                f (interval [(a,b)])
   
   [OPERATIVE_1_LT]  Theorem
      
      ⊢ ∀op.
          monoidal op ⇒
          ∀f. operative op f ⇔
              (∀a b. b ≤ a ⇒ f (interval [(a,b)]) = neutral op) ∧
              ∀a b c.
                a < c ∧ c < b ⇒
                op (f (interval [(a,c)])) (f (interval [(c,b)])) =
                f (interval [(a,b)])
   
   [OPERATIVE_APPROXIMABLE]  Theorem
      
      ⊢ ∀f e.
          0 ≤ e ⇒
          operative $/\
            (λi. ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i)
   
   [OPERATIVE_CONTENT]  Theorem
      
      ⊢ operative $+ content
   
   [OPERATIVE_DIVISION]  Theorem
      
      ⊢ ∀op d a b f.
          monoidal op ∧ operative op f ∧ d division_of interval [(a,b)] ⇒
          iterate op d f = f (interval [(a,b)])
   
   [OPERATIVE_DIVISION_AND]  Theorem
      
      ⊢ ∀P d a b.
          operative $/\ P ∧ d division_of interval [(a,b)] ⇒
          ((∀i. i ∈ d ⇒ P i) ⇔ P (interval [(a,b)]))
   
   [OPERATIVE_EMPTY]  Theorem
      
      ⊢ ∀op f. operative op f ⇒ f ∅ = neutral op
   
   [OPERATIVE_FUNCTION_ENDPOINT_DIFF]  Theorem
      
      ⊢ ∀f. operative $+
              (λk. f (interval_upperbound k) − f (interval_lowerbound k))
   
   [OPERATIVE_INTEGRABLE]  Theorem
      
      ⊢ ∀f. operative $/\ (λi. f integrable_on i)
   
   [OPERATIVE_INTEGRAL]  Theorem
      
      ⊢ ∀f. operative (lifted $+)
              (λi. if f integrable_on i then SOME (integral i f) else NONE)
   
   [OPERATIVE_LIFTED_SETVARIATION]  Theorem
      
      ⊢ ∀f. operative $+ f ⇒
            operative (lifted $+)
              (λi.
                   if f has_bounded_setvariation_on i then
                     SOME (set_variation i f)
                   else NONE)
   
   [OPERATIVE_LIFTED_VECTOR_VARIATION]  Theorem
      
      ⊢ ∀f. operative (lifted $+)
              (λi.
                   if f has_bounded_variation_on i then
                     SOME (vector_variation i f)
                   else NONE)
   
   [OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF]  Theorem
      
      ⊢ ∀f. operative $+
              (λk. f (interval_upperbound k) − f (interval_lowerbound k))
   
   [OPERATIVE_TAGGED_DIVISION]  Theorem
      
      ⊢ ∀op d a b f.
          monoidal op ∧ operative op f ∧
          d tagged_division_of interval [(a,b)] ⇒
          iterate op d (λ(x,l). f l) = f (interval [(a,b)])
   
   [OPERATIVE_TRIVIAL]  Theorem
      
      ⊢ ∀op f a b.
          operative op f ∧ content (interval [(a,b)]) = 0 ⇒
          f (interval [(a,b)]) = neutral op
   
   [PARTIAL_DIVISION_EXTEND]  Theorem
      
      ⊢ ∀p q s t.
          p division_of s ∧ q division_of t ∧ s ⊆ t ⇒
          ∃r. p ⊆ r ∧ r division_of t
   
   [PARTIAL_DIVISION_EXTEND_1]  Theorem
      
      ⊢ ∀a b c d.
          interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
          ∃p. p division_of interval [(a,b)] ∧ interval [(c,d)] ∈ p
   
   [PARTIAL_DIVISION_EXTEND_INTERVAL]  Theorem
      
      ⊢ ∀p a b.
          p division_of BIGUNION p ∧ BIGUNION p ⊆ interval [(a,b)] ⇒
          ∃q. p ⊆ q ∧ q division_of interval [(a,b)]
   
   [PARTIAL_DIVISION_OF_TAGGED_DIVISION]  Theorem
      
      ⊢ ∀s i.
          s tagged_partial_division_of i ⇒
          IMAGE SND s division_of BIGUNION (IMAGE SND s)
   
   [PROPERTY_EMPTY_INTERVAL]  Theorem
      
      ⊢ ∀P. (∀a b. content (interval [(a,b)]) = 0 ⇒ P (interval [(a,b)])) ⇒
            P ∅
   
   [REAL_MUL_POS_LT]  Theorem
      
      ⊢ ∀x y. 0 < x * y ⇔ 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0
   
   [REAL_SUP_LE_FINITE]  Theorem
      
      ⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)
   
   [RSUM_BOUND]  Theorem
      
      ⊢ ∀p a b f e.
          p tagged_division_of interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ abs (f x) ≤ e) ⇒
          abs (sum p (λ(x,k). content k * f x)) ≤
          e * content (interval [(a,b)])
   
   [RSUM_COMPONENT_LE]  Theorem
      
      ⊢ ∀p a b f g.
          p tagged_division_of interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ f x ≤ g x) ⇒
          sum p (λ(x,k). content k * f x) ≤ sum p (λ(x,k). content k * g x)
   
   [RSUM_DIFF_BOUND]  Theorem
      
      ⊢ ∀e p a b f g.
          p tagged_division_of interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ abs (f x − g x) ≤ e) ⇒
          abs
            (sum p (λ(x,k). content k * f x) −
             sum p (λ(x,k). content k * g x)) ≤
          e * content (interval [(a,b)])
   
   [SECOND_MEAN_VALUE_THEOREM]  Theorem
      
      ⊢ ∀f g a b.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              integral (interval [(a,b)]) (λx. g x * f x) =
              g a * integral (interval [(a,c)]) f +
              g b * integral (interval [(c,b)]) f
   
   [SECOND_MEAN_VALUE_THEOREM_BONNET]  Theorem
      
      ⊢ ∀f g a b.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              integral (interval [(a,b)]) (λx. g x * f x) =
              g b * integral (interval [(c,b)]) f
   
   [SECOND_MEAN_VALUE_THEOREM_BONNET_FULL]  Theorem
      
      ⊢ ∀f g a b.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval [(a,b)] ⇒ 0 ≤ g x) ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              ((λx. g x * f x) has_integral
               g b * integral (interval [(c,b)]) f) (interval [(a,b)])
   
   [SECOND_MEAN_VALUE_THEOREM_FULL]  Theorem
      
      ⊢ ∀f g a b.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              ((λx. g x * f x) has_integral
               g a * integral (interval [(a,c)]) f +
               g b * integral (interval [(c,b)]) f) (interval [(a,b)])
   
   [SECOND_MEAN_VALUE_THEOREM_GEN]  Theorem
      
      ⊢ ∀f g a b u v.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              integral (interval [(a,b)]) (λx. g x * f x) =
              u * integral (interval [(a,c)]) f +
              v * integral (interval [(c,b)]) f
   
   [SECOND_MEAN_VALUE_THEOREM_GEN_FULL]  Theorem
      
      ⊢ ∀f g a b u v.
          interval [(a,b)] ≠ ∅ ∧ f integrable_on interval [(a,b)] ∧
          (∀x. x ∈ interval (a,b) ⇒ u ≤ g x ∧ g x ≤ v) ∧
          (∀x y.
             x ∈ interval [(a,b)] ∧ y ∈ interval [(a,b)] ∧ x ≤ y ⇒
             g x ≤ g y) ⇒
          ∃c. c ∈ interval [(a,b)] ∧
              ((λx. g x * f x) has_integral
               u * integral (interval [(a,c)]) f +
               v * integral (interval [(c,b)]) f) (interval [(a,b)])
   
   [SETVARIATION_EQUAL_LEMMA]  Theorem
      
      ⊢ ∀mf ms ms'.
          (∀s. ms' (ms s) = s ∧ ms (ms' s) = s) ∧
          (∀f a b.
             interval [(a,b)] ≠ ∅ ⇒
             mf f (ms (interval [(a,b)])) = f (interval [(a,b)]) ∧
             ∃a' b'.
               interval [(a',b')] ≠ ∅ ∧
               ms' (interval [(a,b)]) = interval [(a',b')]) ∧
          (∀t u. t ⊆ u ⇒ ms t ⊆ ms u ∧ ms' t ⊆ ms' u) ∧
          (∀d t.
             d division_of t ⇒
             IMAGE ms d division_of ms t ∧ IMAGE ms' d division_of ms' t) ⇒
          (∀f s.
             mf f has_bounded_setvariation_on ms s ⇔
             f has_bounded_setvariation_on s) ∧
          ∀f s. set_variation (ms s) (mf f) = set_variation s f
   
   [SET_VARIATION]  Theorem
      
      ⊢ ∀f s d t.
          f has_bounded_setvariation_on s ∧ d division_of t ∧ t ⊆ s ⇒
          sum d (λk. abs (f k)) ≤ set_variation s f
   
   [SET_VARIATION_0]  Theorem
      
      ⊢ ∀s. set_variation s (λx. 0) = 0
   
   [SET_VARIATION_COMPARISON]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧
          (∀a b.
             interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
             abs (g (interval [(a,b)])) ≤ abs (f (interval [(a,b)]))) ⇒
          set_variation s g ≤ set_variation s f
   
   [SET_VARIATION_ELEMENTARY_LEMMA]  Theorem
      
      ⊢ ∀f s b.
          (∃d. d division_of s) ⇒
          ((∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ b) ⇔
           ∀d. d division_of s ⇒ sum d (λk. abs (f k)) ≤ b)
   
   [SET_VARIATION_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀a b.
             interval [(a,b)] ≠ ∅ ∧ interval [(a,b)] ⊆ s ⇒
             f (interval [(a,b)]) = g (interval [(a,b)])) ⇒
          set_variation s f = set_variation s g
   
   [SET_VARIATION_GE_FUNCTION]  Theorem
      
      ⊢ ∀f s a b.
          f has_bounded_setvariation_on s ∧ interval [(a,b)] ⊆ s ∧
          interval [(a,b)] ≠ ∅ ⇒
          abs (f (interval [(a,b)])) ≤ set_variation s f
   
   [SET_VARIATION_LBOUND]  Theorem
      
      ⊢ ∀f s B.
          f has_bounded_setvariation_on s ∧
          (∃d t. d division_of t ∧ t ⊆ s ∧ B ≤ sum d (λk. abs (f k))) ⇒
          B ≤ set_variation s f
   
   [SET_VARIATION_LBOUND_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b B.
          f has_bounded_setvariation_on interval [(a,b)] ∧
          (∃d. d division_of interval [(a,b)] ∧ B ≤ sum d (λk. abs (f k))) ⇒
          B ≤ set_variation (interval [(a,b)]) f
   
   [SET_VARIATION_MONOTONE]  Theorem
      
      ⊢ ∀f s t.
          f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
          set_variation t f ≤ set_variation s f
   
   [SET_VARIATION_ON_DIVISION]  Theorem
      
      ⊢ ∀f a b d.
          operative $+ f ∧ d division_of interval [(a,b)] ∧
          f has_bounded_setvariation_on interval [(a,b)] ⇒
          sum d (λk. set_variation k f) =
          set_variation (interval [(a,b)]) f
   
   [SET_VARIATION_ON_ELEMENTARY]  Theorem
      
      ⊢ ∀f s.
          (∃d. d division_of s) ⇒
          set_variation s f = sup {sum d (λk. abs (f k)) | d division_of s}
   
   [SET_VARIATION_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          set_variation (interval [(a,b)]) f =
          sup {sum d (λk. abs (f k)) | d division_of interval [(a,b)]}
   
   [SET_VARIATION_ON_NULL]  Theorem
      
      ⊢ ∀f s.
          (∀a b. content (interval [(a,b)]) = 0 ⇒ f (interval [(a,b)]) = 0) ∧
          content s = 0 ∧ bounded s ⇒
          set_variation s f = 0
   
   [SET_VARIATION_POS_LE]  Theorem
      
      ⊢ ∀f s. f has_bounded_setvariation_on s ⇒ 0 ≤ set_variation s f
   
   [SET_VARIATION_REFLECT2]  Theorem
      
      ⊢ ∀f s.
          set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
          set_variation s f
   
   [SET_VARIATION_SUM_LE]  Theorem
      
      ⊢ ∀f s k.
          FINITE k ∧ (∀i. i ∈ k ⇒ f i has_bounded_setvariation_on s) ⇒
          set_variation s (λx. sum k (λi. f i x)) ≤
          sum k (λi. set_variation s (f i))
   
   [SET_VARIATION_TRANSLATION2]  Theorem
      
      ⊢ ∀a f s.
          set_variation (IMAGE (λx. -a + x) s)
            (λk. f (IMAGE (λx. a + x) k)) =
          set_variation s f
   
   [SET_VARIATION_TRIANGLE]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_setvariation_on s ∧ g has_bounded_setvariation_on s ⇒
          set_variation s (λx. f x + g x) ≤
          set_variation s f + set_variation s g
   
   [SET_VARIATION_UBOUND]  Theorem
      
      ⊢ ∀f s B.
          f has_bounded_setvariation_on s ∧
          (∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
          set_variation s f ≤ B
   
   [SET_VARIATION_UBOUND_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b B.
          f has_bounded_setvariation_on interval [(a,b)] ∧
          (∀d. d division_of interval [(a,b)] ⇒ sum d (λk. abs (f k)) ≤ B) ⇒
          set_variation (interval [(a,b)]) f ≤ B
   
   [SET_VARIATION_WORKS_ON_INTERVAL]  Theorem
      
      ⊢ ∀f a b d.
          f has_bounded_setvariation_on interval [(a,b)] ∧
          d division_of interval [(a,b)] ⇒
          sum d (λk. abs (f k)) ≤ set_variation (interval [(a,b)]) f
   
   [SUBADDITIVE_CONTENT_DIVISION]  Theorem
      
      ⊢ ∀d s a b.
          d division_of s ∧ s ⊆ interval [(a,b)] ⇒
          sum d content ≤ content (interval [(a,b)])
   
   [SUM_ABS_ALLSUBSETS_BOUND]  Theorem
      
      ⊢ ∀f p e.
          FINITE p ∧ (∀q. q ⊆ p ⇒ abs (sum q f) ≤ e) ⇒
          sum p (λx. abs (f x)) ≤ 2 * 1 * e
   
   [SUM_CONTENT_AREA_OVER_THIN_DIVISION]  Theorem
      
      ⊢ ∀d a b s c.
          d division_of s ∧ s ⊆ interval [(a,b)] ∧ a ≤ c ∧ c ≤ b ∧
          (∀k. k ∈ d ⇒ k ∩ {x | x = c} ≠ ∅) ⇒
          (b − a) *
          sum d
            (λk.
                 content k /
                 (interval_upperbound k − interval_lowerbound k)) ≤
          2 * content (interval [(a,b)])
   
   [SUM_CONTENT_NULL]  Theorem
      
      ⊢ ∀f a b p.
          content (interval [(a,b)]) = 0 ∧
          p tagged_division_of interval [(a,b)] ⇒
          sum p (λ(x,k). content k * f x) = 0
   
   [SUM_NONZERO_IMAGE_LEMMA]  Theorem
      
      ⊢ ∀s f g a.
          FINITE s ∧ g a = 0 ∧
          (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ∧ x ≠ y ⇒ g (f x) = 0) ⇒
          sum {f x | x | x ∈ s ∧ f x ≠ a} g = sum s (g ∘ f)
   
   [SUM_OVER_TAGGED_DIVISION_LEMMA]  Theorem
      
      ⊢ ∀d p i.
          p tagged_division_of i ∧
          (∀u v.
             interval [(u,v)] ≠ ∅ ∧ content (interval [(u,v)]) = 0 ⇒
             d (interval [(u,v)]) = 0) ⇒
          sum p (λ(x,k). d k) = sum (IMAGE SND p) d
   
   [SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA]  Theorem
      
      ⊢ ∀d p i.
          p tagged_partial_division_of i ∧
          (∀u v.
             interval [(u,v)] ≠ ∅ ∧ content (interval [(u,v)]) = 0 ⇒
             d (interval [(u,v)]) = 0) ⇒
          sum p (λ(x,k). d k) = sum (IMAGE SND p) d
   
   [SUP_FINITE]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s
   
   [SUP_FINITE_LEMMA]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b
   
   [TAGGED_DIVISION_BIGUNION]  Theorem
      
      ⊢ ∀iset pfn.
          FINITE iset ∧ (∀i. i ∈ iset ⇒ pfn i tagged_division_of i) ∧
          (∀i1 i2.
             i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒
             interior i1 ∩ interior i2 = ∅) ⇒
          BIGUNION (IMAGE pfn iset) tagged_division_of BIGUNION iset
   
   [TAGGED_DIVISION_BIGUNION_EXISTS]  Theorem
      
      ⊢ ∀d iset i.
          FINITE iset ∧
          (∀i. i ∈ iset ⇒ ∃p. p tagged_division_of i ∧ d FINE p) ∧
          (∀i1 i2.
             i1 ∈ iset ∧ i2 ∈ iset ∧ i1 ≠ i2 ⇒
             interior i1 ∩ interior i2 = ∅) ∧ BIGUNION iset = i ⇒
          ∃p. p tagged_division_of i ∧ d FINE p
   
   [TAGGED_DIVISION_FINER]  Theorem
      
      ⊢ ∀p a b d.
          p tagged_division_of interval [(a,b)] ∧ gauge d ⇒
          ∃q. q tagged_division_of interval [(a,b)] ∧ d FINE q ∧
              ∀x k. (x,k) ∈ p ∧ k ⊆ d x ⇒ (x,k) ∈ q
   
   [TAGGED_DIVISION_OF]  Theorem
      
      ⊢ ∀s i.
          s tagged_division_of i ⇔
          FINITE s ∧
          (∀x k. (x,k) ∈ s ⇒ x ∈ k ∧ k ⊆ i ∧ ∃a b. k = interval [(a,b)]) ∧
          (∀x1 k1 x2 k2.
             (x1,k1) ∈ s ∧ (x2,k2) ∈ s ∧ (x1,k1) ≠ (x2,k2) ⇒
             interior k1 ∩ interior k2 = ∅) ∧
          BIGUNION {k | (∃x. (x,k) ∈ s)} = i
   
   [TAGGED_DIVISION_OF_ALT]  Theorem
      
      ⊢ ∀p s.
          p tagged_division_of s ⇔
          p tagged_partial_division_of s ∧
          ∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k
   
   [TAGGED_DIVISION_OF_ANOTHER]  Theorem
      
      ⊢ ∀p s s'.
          p tagged_partial_division_of s' ∧ (∀t k. (t,k) ∈ p ⇒ k ⊆ s) ∧
          (∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k) ⇒
          p tagged_division_of s
   
   [TAGGED_DIVISION_OF_EMPTY]  Theorem
      
      ⊢ ∅ tagged_division_of ∅
   
   [TAGGED_DIVISION_OF_FINITE]  Theorem
      
      ⊢ ∀s i. s tagged_division_of i ⇒ FINITE s
   
   [TAGGED_DIVISION_OF_NONTRIVIAL]  Theorem
      
      ⊢ ∀s a b.
          s tagged_division_of interval [(a,b)] ∧
          content (interval [(a,b)]) ≠ 0 ⇒
          {(x,k) | (x,k) ∈ s ∧ content k ≠ 0} tagged_division_of
          interval [(a,b)]
   
   [TAGGED_DIVISION_OF_SELF]  Theorem
      
      ⊢ ∀x a b.
          x ∈ interval [(a,b)] ⇒
          {(x,interval [(a,b)])} tagged_division_of interval [(a,b)]
   
   [TAGGED_DIVISION_OF_TRIVIAL]  Theorem
      
      ⊢ ∀p. p tagged_division_of ∅ ⇔ p = ∅
   
   [TAGGED_DIVISION_OF_UNION_SELF]  Theorem
      
      ⊢ ∀p s.
          p tagged_division_of s ⇒
          p tagged_division_of BIGUNION (IMAGE SND p)
   
   [TAGGED_DIVISION_SPLIT_LEFT_INJ]  Theorem
      
      ⊢ ∀d i x1 k1 x2 k2 c.
          d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
          k1 ∩ {x | x ≤ c} = k2 ∩ {x | x ≤ c} ⇒
          content (k1 ∩ {x | x ≤ c}) = 0
   
   [TAGGED_DIVISION_SPLIT_RIGHT_INJ]  Theorem
      
      ⊢ ∀d i x1 k1 x2 k2 c.
          d tagged_division_of i ∧ (x1,k1) ∈ d ∧ (x2,k2) ∈ d ∧ k1 ≠ k2 ∧
          k1 ∩ {x | x ≥ c} = k2 ∩ {x | x ≥ c} ⇒
          content (k1 ∩ {x | x ≥ c}) = 0
   
   [TAGGED_DIVISION_UNION]  Theorem
      
      ⊢ ∀s1 s2 p1 p2.
          p1 tagged_division_of s1 ∧ p2 tagged_division_of s2 ∧
          interior s1 ∩ interior s2 = ∅ ⇒
          p1 ∪ p2 tagged_division_of s1 ∪ s2
   
   [TAGGED_DIVISION_UNION_IMAGE_SND]  Theorem
      
      ⊢ ∀p s. p tagged_division_of s ⇒ s = BIGUNION (IMAGE SND p)
   
   [TAGGED_DIVISION_UNION_INTERVAL]  Theorem
      
      ⊢ ∀a b p1 p2 c.
          p1 tagged_division_of interval [(a,b)] ∩ {x | x ≤ c} ∧
          p2 tagged_division_of interval [(a,b)] ∩ {x | x ≥ c} ⇒
          p1 ∪ p2 tagged_division_of interval [(a,b)]
   
   [TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND]  Theorem
      
      ⊢ ∀p s y.
          p tagged_partial_division_of s ⇒
          CARD {(x,k) | (x,k) ∈ p ∧ y ∈ k ∧ content k ≠ 0} ≤ 2 ** 1
   
   [TAGGED_PARTIAL_DIVISION_COMMON_TAGS]  Theorem
      
      ⊢ ∀p s x.
          p tagged_partial_division_of s ⇒
          CARD {(x,k) | k | (x,k) ∈ p ∧ content k ≠ 0} ≤ 2 ** 1
   
   [TAGGED_PARTIAL_DIVISION_OF_SUBSET]  Theorem
      
      ⊢ ∀p s t.
          p tagged_partial_division_of s ∧ s ⊆ t ⇒
          p tagged_partial_division_of t
   
   [TAGGED_PARTIAL_DIVISION_OF_TRIVIAL]  Theorem
      
      ⊢ ∀p. p tagged_partial_division_of ∅ ⇔ p = ∅
   
   [TAGGED_PARTIAL_DIVISION_OF_UNION_SELF]  Theorem
      
      ⊢ ∀p s.
          p tagged_partial_division_of s ⇒
          p tagged_division_of BIGUNION (IMAGE SND p)
   
   [TAGGED_PARTIAL_DIVISION_SUBSET]  Theorem
      
      ⊢ ∀s t i.
          s tagged_partial_division_of i ∧ t ⊆ s ⇒
          t tagged_partial_division_of i
   
   [TAG_IN_INTERVAL]  Theorem
      
      ⊢ ∀p i k. p tagged_division_of i ∧ (x,k) ∈ p ⇒ x ∈ i
   
   [VARIATION_EQUAL_LEMMA]  Theorem
      
      ⊢ ∀ms ms'.
          (∀s. ms' (ms s) = s ∧ ms (ms' s) = s) ∧
          (∀d t.
             d division_of t ⇒
             IMAGE (IMAGE ms) d division_of IMAGE ms t ∧
             IMAGE (IMAGE ms') d division_of IMAGE ms' t) ∧
          (∀a b.
             interval [(a,b)] ≠ ∅ ⇒
             IMAGE ms' (interval [(a,b)]) = interval [(ms' a,ms' b)] ∨
             IMAGE ms' (interval [(a,b)]) = interval [(ms' b,ms' a)]) ⇒
          (∀f s.
             (λx. f (ms' x)) has_bounded_variation_on IMAGE ms s ⇔
             f has_bounded_variation_on s) ∧
          ∀f s.
            vector_variation (IMAGE ms s) (λx. f (ms' x)) =
            vector_variation s f
   
   [VECTOR_VARIATION_ABS]  Theorem
      
      ⊢ ∀f s.
          (λx. f x) has_bounded_variation_on s ⇒
          vector_variation s (λx. abs (f x)) ≤ vector_variation s (λx. f x)
   
   [VECTOR_VARIATION_AFFINITY]  Theorem
      
      ⊢ ∀m c f s.
          vector_variation s (λx. f (m * x + c)) =
          if m = 0 then 0 else vector_variation (IMAGE (λx. m * x + c) s) f
   
   [VECTOR_VARIATION_AFFINITY2]  Theorem
      
      ⊢ ∀m c f s.
          vector_variation (IMAGE (λx. m⁻¹ * x + -(m⁻¹ * c)) s)
            (λx. f (m * x + c)) =
          if m = 0 then 0 else vector_variation s f
   
   [VECTOR_VARIATION_COMBINE]  Theorem
      
      ⊢ ∀f a b c.
          a ≤ c ∧ c ≤ b ∧ f has_bounded_variation_on interval [(a,b)] ⇒
          vector_variation (interval [(a,c)]) f +
          vector_variation (interval [(c,b)]) f =
          vector_variation (interval [(a,b)]) f
   
   [VECTOR_VARIATION_COMPARISON]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧
          (∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ dist (g x,g y) ≤ dist (f x,f y)) ⇒
          vector_variation s g ≤ vector_variation s f
   
   [VECTOR_VARIATION_CONST]  Theorem
      
      ⊢ ∀s c. vector_variation s (λx. c) = 0
   
   [VECTOR_VARIATION_CONST_EQ]  Theorem
      
      ⊢ ∀f s.
          is_interval s ∧ f has_bounded_variation_on s ⇒
          (vector_variation s f = 0 ⇔ ∃c. ∀x. x ∈ s ⇒ f x = c)
   
   [VECTOR_VARIATION_CONTINUOUS]  Theorem
      
      ⊢ ∀f a b c.
          f has_bounded_variation_on interval [(a,b)] ∧
          c ∈ interval [(a,b)] ⇒
          ((λx. vector_variation (interval [(a,x)]) f) continuous
           (at c within interval [(a,b)]) ⇔
           f continuous (at c within interval [(a,b)]))
   
   [VECTOR_VARIATION_CONTINUOUS_LEFT]  Theorem
      
      ⊢ ∀f a b c.
          f has_bounded_variation_on interval [(a,b)] ∧
          c ∈ interval [(a,b)] ⇒
          ((λx. vector_variation (interval [(a,x)]) f) continuous
           (at c within interval [(a,c)]) ⇔
           f continuous (at c within interval [(a,c)]))
   
   [VECTOR_VARIATION_CONTINUOUS_RIGHT]  Theorem
      
      ⊢ ∀f a b c.
          f has_bounded_variation_on interval [(a,b)] ∧
          c ∈ interval [(a,b)] ⇒
          ((λx. vector_variation (interval [(a,x)]) f) continuous
           (at c within interval [(c,b)]) ⇔
           f continuous (at c within interval [(c,b)]))
   
   [VECTOR_VARIATION_EQ]  Theorem
      
      ⊢ ∀f g s.
          (∀x. x ∈ s ⇒ f x = g x) ⇒
          vector_variation s f = vector_variation s g
   
   [VECTOR_VARIATION_GE_ABS_FUNCTION]  Theorem
      
      ⊢ ∀f s a b.
          f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
          abs (f b − f a) ≤ vector_variation s f
   
   [VECTOR_VARIATION_GE_FUNCTION]  Theorem
      
      ⊢ ∀f s a b.
          f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
          f b − f a ≤ vector_variation s f
   
   [VECTOR_VARIATION_MINUS_FUNCTION_MONOTONE]  Theorem
      
      ⊢ ∀f a b c d.
          f has_bounded_variation_on interval [(a,b)] ∧
          interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
          vector_variation (interval [(c,d)]) f − (f d − f c) ≤
          vector_variation (interval [(a,b)]) f − (f b − f a)
   
   [VECTOR_VARIATION_MONOTONE]  Theorem
      
      ⊢ ∀f s t.
          f has_bounded_variation_on s ∧ t ⊆ s ⇒
          vector_variation t f ≤ vector_variation s f
   
   [VECTOR_VARIATION_NEG]  Theorem
      
      ⊢ ∀f s. vector_variation s (λx. -f x) = vector_variation s f
   
   [VECTOR_VARIATION_ON_DIVISION]  Theorem
      
      ⊢ ∀f a b d.
          d division_of interval [(a,b)] ∧
          f has_bounded_variation_on interval [(a,b)] ⇒
          sum d (λk. vector_variation k f) =
          vector_variation (interval [(a,b)]) f
   
   [VECTOR_VARIATION_ON_NULL]  Theorem
      
      ⊢ ∀f s. content s = 0 ∧ bounded s ⇒ vector_variation s f = 0
   
   [VECTOR_VARIATION_POS_LE]  Theorem
      
      ⊢ ∀f s. f has_bounded_variation_on s ⇒ 0 ≤ vector_variation s f
   
   [VECTOR_VARIATION_REFLECT]  Theorem
      
      ⊢ ∀f s.
          vector_variation s (λx. f (-x)) =
          vector_variation (IMAGE (λx. -x) s) f
   
   [VECTOR_VARIATION_REFLECT2]  Theorem
      
      ⊢ ∀f s.
          vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) =
          vector_variation s f
   
   [VECTOR_VARIATION_REFLECT_INTERVAL]  Theorem
      
      ⊢ ∀f a b.
          vector_variation (interval [(a,b)]) (λx. f (-x)) =
          vector_variation (interval [(-b,-a)]) f
   
   [VECTOR_VARIATION_TRANSLATION]  Theorem
      
      ⊢ ∀a f s.
          vector_variation s (λx. f (a + x)) =
          vector_variation (IMAGE (λx. a + x) s) f
   
   [VECTOR_VARIATION_TRANSLATION2]  Theorem
      
      ⊢ ∀a f s.
          vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
          vector_variation s f
   
   [VECTOR_VARIATION_TRANSLATION_INTERVAL]  Theorem
      
      ⊢ ∀a f u v.
          vector_variation (interval [(u,v)]) (λx. f (a + x)) =
          vector_variation (interval [(a + u,a + v)]) f
   
   [VECTOR_VARIATION_TRIANGLE]  Theorem
      
      ⊢ ∀f g s.
          f has_bounded_variation_on s ∧ g has_bounded_variation_on s ⇒
          vector_variation s (λx. f x + g x) ≤
          vector_variation s f + vector_variation s g
   
   [has_integral]  Theorem
      
      ⊢ (f has_integral y) (interval [(a,b)]) ⇔
        ∀e. 0 < e ⇒
            ∃d. gauge d ∧
                ∀p. p tagged_division_of interval [(a,b)] ∧ d FINE p ⇒
                    abs (sum p (λ(x,k). content k * f x) − y) < e
   
   [has_integral_alt]  Theorem
      
      ⊢ (f has_integral y) i ⇔
        if ∃a b. i = interval [(a,b)] then (f has_integral y) i
        else
          ∀e. 0 < e ⇒
              ∃B. 0 < B ∧
                  ∀a b.
                    ball (0,B) ⊆ interval [(a,b)] ⇒
                    ∃z. ((λx. if x ∈ i then f x else 0) has_integral z)
                          (interval [(a,b)]) ∧ abs (z − y) < e
   
   [lifted_def]  Theorem
      
      ⊢ lifted op NONE v0 = NONE ∧ lifted op (SOME v5) NONE = NONE ∧
        lifted op (SOME x) (SOME y) = SOME (op x y)
   
   [lifted_ind]  Theorem
      
      ⊢ ∀P. (∀op v0. P op NONE v0) ∧ (∀op v5. P op (SOME v5) NONE) ∧
            (∀op x y. P op (SOME x) (SOME y)) ⇒
            ∀v v1 v2. P v v1 v2
   
   
*)
end

HOL 4, Kananaskis-14