Theory integration

⊢ ∀d s. d FINE s ⇔ ∀x k. (x,k) ∈ s ⇒ k ⊆ d x

⊢ ∀f s.
    f absolutely_integrable_on s ⇔
    f integrable_on s ∧ (λx. abs (f x)) integrable_on s

⊢ ∀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

⊢ ∀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)}

⊢ ∀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

⊢ ∀d. gauge d ⇔ ∀x. x ∈ d x ∧ open (d x)

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇔
    ∃B. ∀d t. d division_of t ∧ t ⊆ s ⇒ sum d (λk. abs (f k)) ≤ B

⊢ ∀f s.
    f has_bounded_variation_on s ⇔
    (λk. f (interval_upperbound k) − f (interval_lowerbound k)) has_bounded_setvariation_on
    s

⊢ ∀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

⊢ ∀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

⊢ ∀f i. f integrable_on i ⇔ ∃y. (f has_integral y) i

⊢ ∀i f. integral i f = @y. (f has_integral y) i

⊢ ∀s. negligible s ⇔ ∀a b. (indicator s has_integral 0) (interval [(a,b)])

⊢ ∀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}))

⊢ ∀s f.
    set_variation s f =
    sup {sum d (λk. abs (f k)) | (∃t. d division_of t ∧ t ⊆ s)}

⊢ ∀s i.
    s tagged_division_of i ⇔
    s tagged_partial_division_of i ∧ BIGUNION {k | (∃x. (x,k) ∈ s)} = i

⊢ ∀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 = ∅

⊢ ∀s f.
    vector_variation s f =
    set_variation s
      (λk. f (interval_upperbound k) − f (interval_lowerbound k))

⊢ ∀s. (λx. 0) absolutely_integrable_on s

⊢ ∀f s.
    f absolutely_integrable_on s ⇒
    (λx. abs (f x)) absolutely_integrable_on s

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f absolutely_integrable_on s ∧
    g integrable_on s ⇒
    g absolutely_integrable_on s

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x ≤ g x) ∧ f integrable_on s ∧
    g absolutely_integrable_on s ⇒
    f absolutely_integrable_on s

⊢ ∀f s.
    f absolutely_integrable_on s ⇔
    f integrable_on s ∧ (λx. abs (f x)) integrable_on s

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. f x + g x) absolutely_integrable_on s

⊢ ∀f s.
    f absolutely_integrable_on s ⇒
    (λk. integral k f) has_bounded_setvariation_on s

⊢ ∀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)]

⊢ ∀f. f absolutely_integrable_on 𝕌(:real) ⇔
      f integrable_on 𝕌(:real) ∧
      (λk. integral k f) has_bounded_setvariation_on 𝕌(:real)

⊢ ∀f s c.
    f absolutely_integrable_on s ⇒ (λx. c * f x) absolutely_integrable_on s

⊢ ∀f s. f absolutely_integrable_on s ⇔ (λx. f x) absolutely_integrable_on s

⊢ ∀a b c. (λx. c) absolutely_integrable_on interval [(a,b)]

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    f absolutely_integrable_on interval [(a,b)]

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x = g x) ∧ f absolutely_integrable_on s ⇒
    g absolutely_integrable_on s

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x = g x) ⇒
    (f absolutely_integrable_on s ⇔ g absolutely_integrable_on s)

⊢ ∀f s. f absolutely_integrable_on s ⇒ (λx. abs (f x)) integrable_on s

⊢ ∀f s. f absolutely_integrable_on s ⇒ f integrable_on s

⊢ ∀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

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ∧ f integrable_on s ∧ g integrable_on s ⇒
    f absolutely_integrable_on s

⊢ ∀f s.
    f absolutely_integrable_on s ⇒
    abs (integral s f) ≤ integral s (λx. abs (f x))

⊢ ∀f h s.
    f absolutely_integrable_on s ∧ linear h ⇒
    h ∘ f absolutely_integrable_on s

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. max (f x) (g x)) absolutely_integrable_on s

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. min (f x) (g x)) absolutely_integrable_on s

⊢ ∀f s.
    (λx. f x * indicator s x) absolutely_integrable_on 𝕌(:real) ⇔
    f absolutely_integrable_on s

⊢ ∀f s.
    f absolutely_integrable_on s ⇒ (λx. -f x) absolutely_integrable_on s

⊢ ∀f a b.
    content (interval [(a,b)]) = 0 ⇒
    f absolutely_integrable_on interval [(a,b)]

⊢ ∀f s a b.
    f absolutely_integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
    f absolutely_integrable_on interval [(a,b)]

⊢ ∀f s t.
    (λx. if x ∈ s then f x else 0) absolutely_integrable_on t ⇔
    f absolutely_integrable_on s ∩ t

⊢ ∀f s.
    (λx. if x ∈ s then f x else 0) absolutely_integrable_on 𝕌(:real) ⇔
    f absolutely_integrable_on s

⊢ ∀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))

⊢ ∀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

⊢ ∀f g s.
    f absolutely_integrable_on s ∧ g absolutely_integrable_on s ⇒
    (λx. f x − g x) absolutely_integrable_on s

⊢ ∀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

⊢ ∀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

⊢ ∀d a b.
    d division_of interval [(a,b)] ⇒
    sum d content = content (interval [(a,b)])

⊢ ∀d a b.
    d tagged_division_of interval [(a,b)] ⇒
    sum d (λ(x,l). content l) = content (interval [(a,b)])

⊢ ∀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

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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)]

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f. f integrable_on 𝕌(:real) ∧
      (λk. integral k f) has_bounded_setvariation_on 𝕌(:real) ⇒
      f absolutely_integrable_on 𝕌(:real)

⊢ ∀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)]

⊢ ∀a b c e.
    0 < e ⇒
    ∃d. 0 < d ∧ content (interval [(a,b)] ∩ {x | abs (x − c) ≤ d}) < e

⊢ ∀a b m c.
    content (IMAGE (λx. m * x + c) (interval [(a,b)])) =
    abs m pow 1 * content (interval [(a,b)])

⊢ ∀a b m.
    content (IMAGE (λx. m 1 * x) (interval [(a,b)])) =
    abs (product {1 .. 1} m) * content (interval [(a,b)])

⊢ ∀a b k.
    content (interval [(a,b)]) =
    content (interval [(a,b)] ∩ {x | x ≤ c}) +
    content (interval [(a,b)] ∩ {x | x ≥ c})

⊢ ∀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)]

⊢ ∀s. convex s ⇔ ∀a b. a ∈ s ∧ b ∈ s ⇒ segment [(a,b)] ⊆ s

⊢ ∀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)]

⊢ ∀f s.
    bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f y ≤ f x) ⇒
    f has_bounded_variation_on s

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀d s x.
    d division_of s ⇒ CARD {k | k ∈ d ∧ content k ≠ 0 ∧ x ∈ k} ≤ 2 ** 1

⊢ ∀s i. s division_of i ⇒ ∀x. x ∈ i ⇒ ∃k. x ∈ k ∧ k ∈ s

⊢ ∀s1 s2 p1 p2.
    p1 division_of s1 ∧ p2 division_of s2 ∧ interior s1 ∩ interior s2 = ∅ ⇒
    p1 ∪ p2 division_of s1 ∪ s2

⊢ ∀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}

⊢ ∀s1 s2 p1 p2.
    p1 division_of s1 ∧ p2 division_of s2 ⇒
    {k1 ∩ k2 | k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ ∅} division_of s1 ∩ s2

⊢ ∀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)]

⊢ ∀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

⊢ ∀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

⊢ ∀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)

⊢ ∀s i. s division_of i ⇒ closed i

⊢ ∀a b d.
    content (interval [(a,b)]) = 0 ∧ d division_of interval [(a,b)] ⇒
    ∀k. k ∈ d ⇒ content k = 0

⊢ ∀s i. s division_of i ⇒ FINITE s

⊢ ∀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)]

⊢ ∀d s.
    IMAGE (IMAGE (λx. -x)) d division_of IMAGE (λx. -x) s ⇔ d division_of s

⊢ ∀a b.
    interval [(a,b)] ≠ ∅ ⇒ {interval [(a,b)]} division_of interval [(a,b)]

⊢ ∀s a. s division_of interval [(a,a)] ⇔ s = {interval [(a,a)]}

⊢ ∀p q. p division_of BIGUNION p ∧ q ⊆ p ⇒ q division_of BIGUNION q

⊢ ∀s i. s tagged_division_of i ⇒ IMAGE SND s division_of i

⊢ ∀d s.
    IMAGE (IMAGE (λx. a + x)) d division_of IMAGE (λx. a + x) s ⇔
    d division_of s

⊢ ∀s. s division_of ∅ ⇔ s = ∅

⊢ ∀p s. p division_of s ⇒ p division_of BIGUNION p

⊢ ∀d i. d division_of i ⇒ FINITE (division_points i d)

⊢ ∀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

⊢ ∀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

⊢ ∀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}

⊢ ∀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) ∧
  ∀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

⊢ ∀a b c d.
    interval [(a,b)] ≠ ∅ ⇒
    ∃p. interval [(a,b)] INSERT p division_of
        interval [(a,b)] ∪ interval [(c,d)]

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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)])

⊢ ∀f. FINITE f ∧ f ≠ ∅ ∧ (∀s. s ∈ f ⇒ ∃p. p division_of s) ⇒
      ∃p. p division_of BIGINTER f

⊢ ∀f. FINITE f ∧ (∀s. s ∈ f ⇒ ∃a b. s = interval [(a,b)]) ⇒
      ∃p. p division_of BIGUNION f

⊢ ∀s. (∃p. p division_of s) ⇒ bounded s

⊢ ∀s. (∃d. d division_of s) ⇒ compact s

⊢ ∃p. p division_of ∅

⊢ ∀s t.
    (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒ ∃p. p division_of s ∩ t

⊢ ∀a b. ∃p. p division_of interval [(a,b)]

⊢ ∀s. (∃p. p division_of s) ⇒ ∃a b. s ⊆ interval [(a,b)]

⊢ ∀s t.
    (∃p. p division_of s) ∧ (∃p. p division_of t) ⇒ ∃p. p division_of s ∪ t

⊢ ∀p a b.
    p division_of BIGUNION p ⇒
    ∃q. q division_of interval [(a,b)] ∪ BIGUNION p

⊢ ∀p a b.
    p division_of BIGUNION p ⇒
    ∃q. p ⊆ q ∧ q division_of interval [(a,b)] ∪ BIGUNION p

⊢ ∀s. ∅ division_of s ⇔ s = ∅

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    {(λx. f x + g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s

⊢ ∀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)]

⊢ ∀fs s k.
    fs equiintegrable_on s ⇒
    {(λx. c * f x) | abs c ≤ k ∧ f ∈ fs} equiintegrable_on s

⊢ ∀fs d a b.
    d division_of interval [(a,b)] ⇒
    (fs equiintegrable_on interval [(a,b)] ⇔
     ∀i. i ∈ d ⇒ fs equiintegrable_on i)

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧
    (∀g. g ∈ gs ⇒ ∃f. f ∈ fs ∧ ∀x. x ∈ s ⇒ f x = g x) ⇒
    gs equiintegrable_on s

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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

⊢ ∀fs s. fs equiintegrable_on s ⇒ {(λx. -f x) | f ∈ fs} equiintegrable_on s

⊢ ∀fs a b.
    content (interval [(a,b)]) = 0 ⇒ fs equiintegrable_on interval [(a,b)]

⊢ ∀f a b.
    {f} equiintegrable_on interval [(a,b)] ⇔
    f integrable_on interval [(a,b)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀fs a b.
    fs equiintegrable_on interval [(a,b)] ⇒
    {(λx. f (-x)) | f ∈ fs} equiintegrable_on interval [(-b,-a)]

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    {(λx. f x − g x) | f ∈ fs ∧ g ∈ gs} equiintegrable_on s

⊢ ∀fs gs s. fs equiintegrable_on s ∧ gs ⊆ fs ⇒ gs equiintegrable_on s

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀fs gs s.
    fs equiintegrable_on s ∧ gs equiintegrable_on s ⇒
    fs ∪ gs equiintegrable_on s

⊢ ∀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

⊢ ∀f s p. (λx. BIGINTER {f d x | d ∈ s}) FINE p ⇔ ∀d. d ∈ s ⇒ f d FINE p

⊢ ∀d ps. (∀p. p ∈ ps ⇒ d FINE p) ⇒ d FINE BIGUNION ps

⊢ ∀g a b. gauge g ⇒ ∃p. p tagged_division_of interval [(a,b)] ∧ g FINE p

⊢ ∀p d1 d2. (λx. d1 x ∩ d2 x) FINE p ⇔ d1 FINE p ∧ d2 FINE p

⊢ ∀d p q. p ⊆ q ∧ d FINE q ⇒ d FINE p

⊢ ∀d p1 p2. d FINE p1 ∧ d FINE p2 ⇒ d FINE p1 ∪ p2

⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}

⊢ ∀x. 0 ≤ x ⇒ ∃n. flr x = n

⊢ ∀P d i.
    d division_of i ⇒
    ((∀x. x ∈ d ⇒ P x) ⇔ ∀a b. interval [(a,b)] ∈ d ⇒ P (interval [(a,b)]))

⊢ ∀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)]))

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀e. 0 < e ⇒ gauge (λx. ball (x,e))

⊢ ∀e. (∀x. 0 < e x) ⇒ gauge (λx. ball (x,e x))

⊢ ∀f s.
    FINITE s ∧ (∀d. d ∈ s ⇒ gauge (f d)) ⇒
    gauge (λx. BIGINTER {f d x | d ∈ s})

⊢ ∀p q. (∀x. ∃d. p x ⇒ 0 < d ∧ q d x) ⇔ ∀x. ∃d. 0 < d ∧ (p x ⇒ q d x)

⊢ ∀d1 d2. gauge d1 ∧ gauge d2 ⇒ gauge (λx. d1 x ∩ d2 x)

⊢ ∀f. (∀s. open s ⇒ open {x | f x ∈ s}) ⇒
      ∀d. gauge d ⇒ gauge (λx y. d (f x) (f y))

⊢ gauge (λx. ball (x,1))

⊢ ∀f s y.
    f absolutely_integrable_on s ∧ integral s f = y ⇔
    f absolutely_integrable_on s ∧ (f has_integral y) s

⊢ ∀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

⊢ ∀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

⊢ ∀s. (λx. 0) has_bounded_setvariation_on s

⊢ ∀f s.
    (λx. abs (f x)) has_bounded_setvariation_on s ⇔
    f has_bounded_setvariation_on s

⊢ ∀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

⊢ ∀f c s.
    f has_bounded_setvariation_on s ⇒
    (λx. c * f x) has_bounded_setvariation_on s

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇔
    (λk. f k) has_bounded_setvariation_on s

⊢ ∀f g s.
    f has_bounded_setvariation_on s ∧ linear g ⇒
    g ∘ f has_bounded_setvariation_on s

⊢ ∀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)])

⊢ ∀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)

⊢ ∀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

⊢ ∀f s.
    f has_bounded_setvariation_on s ⇒
    bounded {f (interval [(c,d)]) | interval [(c,d)] ⊆ s}

⊢ ∀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

⊢ ∀f s.
    (λx. -f x) has_bounded_setvariation_on s ⇔
    f has_bounded_setvariation_on s

⊢ ∀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

⊢ ∀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

⊢ ∀f s t.
    f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
    f has_bounded_setvariation_on t

⊢ ∀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) ⇒
     (λ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))

⊢ ∀f. f has_bounded_setvariation_on 𝕌(:real) ⇔
      ∃B. ∀d. d division_of BIGUNION d ⇒ sum d (λk. abs (f k)) ≤ B

⊢ ∀f s.
    (λk. f (IMAGE (λx. -x) k)) has_bounded_setvariation_on IMAGE (λx. -x) s ⇔
    f has_bounded_setvariation_on s

⊢ (∀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

⊢ ∀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

⊢ ∀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.
     (λ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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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.
     (λ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

⊢ ∀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.
     (λ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

⊢ ∀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

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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

⊢ ∀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

⊢ ∀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)])

⊢ ∀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

⊢ ∀f s.
    f has_bounded_variation_on s ⇒
    (λx. abs (f x)) has_bounded_variation_on s

⊢ ∀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

⊢ ∀f s.
    is_interval s ∧ f has_bounded_variation_on s ⇒
    f has_bounded_variation_on closure s

⊢ ∀f c s.
    f has_bounded_variation_on s ⇒ (λx. c * f x) has_bounded_variation_on s

⊢ ∀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)])

⊢ ∀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})

⊢ ∀f s. f has_bounded_variation_on s ⇔ (λx. f x) has_bounded_variation_on s

⊢ ∀f g s.
    f has_bounded_variation_on s ∧ linear g ⇒
    g ∘ f has_bounded_variation_on s

⊢ ∀s c. (λx. c) has_bounded_variation_on s

⊢ ∀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)])

⊢ ∀f. f has_bounded_variation_on ∅

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x = g x) ∧ f has_bounded_variation_on s ⇒
    g has_bounded_variation_on s

⊢ ∀a b. (λx. x) has_bounded_variation_on interval [(a,b)]

⊢ ∀f s. f has_bounded_variation_on s ∧ is_interval s ⇒ bounded (IMAGE f s)

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇒
    bounded (IMAGE f (interval [(a,b)]))

⊢ ∀f s.
    f has_bounded_variation_on s ⇒
    bounded {f d − f c | interval [(c,d)] ⊆ s ∧ interval [(c,d)] ≠ ∅}

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇒
    (λc. integral (interval [(c,b)]) f) has_bounded_variation_on
    interval [(a,b)]

⊢ ∀f a b.
    f absolutely_integrable_on interval [(a,b)] ⇒
    (λc. integral (interval [(a,c)]) f) has_bounded_variation_on
    interval [(a,b)]

⊢ ∀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

⊢ ∀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

⊢ ∀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)]

⊢ ∀f s.
    f has_bounded_variation_on s ⇒ (λx. -f x) has_bounded_variation_on s

⊢ ∀f s. content s = 0 ∧ bounded s ⇒ f has_bounded_variation_on s

⊢ ∀f s.
    f has_bounded_variation_on IMAGE (λx. -x) s ⇒
    (λx. f (-x)) has_bounded_variation_on s

⊢ ∀f a b.
    f has_bounded_variation_on interval [(-b,-a)] ⇒
    (λx. f (-x)) has_bounded_variation_on interval [(a,b)]

⊢ ∀f a. f has_bounded_variation_on {a}

⊢ ∀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

⊢ ∀f s t.
    f has_bounded_variation_on s ∧ t ⊆ s ⇒ f has_bounded_variation_on t

⊢ ∀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) ⇒
     (λ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))

⊢ ∀f s.
    (λx. f (-x)) has_bounded_variation_on IMAGE (λx. -x) s ⇔
    f has_bounded_variation_on s

⊢ (∀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

⊢ ∀f s.
    (λx. f (-x)) has_bounded_variation_on s ⇔
    f has_bounded_variation_on IMAGE (λx. -x) s

⊢ (∀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

⊢ ∀f u v.
    (λx. f (-x)) has_bounded_variation_on interval [(u,v)] ⇔
    f has_bounded_variation_on interval [(-v,-u)]

⊢ (∀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

⊢ ∀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))

⊢ ∀f s a.
    f has_bounded_variation_on s ⇒
    (λx. f (a + x)) has_bounded_variation_on IMAGE (λx. -a + x) s

⊢ ∀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.
     (λ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

⊢ ∀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.
     (λ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

⊢ ∀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.
     (λ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

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀s. ((λx. 0) has_integral 0) s

⊢ ∀i s. ((λx. 0) has_integral i) s ⇔ i = 0

⊢ ∀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

⊢ ∀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

⊢ ∀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)]))

⊢ ∀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

⊢ ∀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)

⊢ ∀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)])

⊢ ∀f y s.
    negligible (frontier s) ⇒
    ((f has_integral y) (closure s) ⇔ (f has_integral y) s)

⊢ ∀f k s c. (f has_integral k) s ⇒ ((λx. c * f x) has_integral c * k) s

⊢ ∀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)])

⊢ ∀f s d i.
    d division_of s ∧ (∀k. k ∈ d ⇒ (f has_integral i k) k) ⇒
    (f has_integral sum d i) s

⊢ ∀f s d k.
    f integrable_on s ∧ d division_of k ∧ k ⊆ s ⇒
    (f has_integral sum d (λi. integral i f)) k

⊢ ∀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

⊢ ∀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)])

⊢ ∀f s y. (f has_integral y) s ⇔ ((λx. f x) has_integral y) s

⊢ ∀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

⊢ ∀f g s i j.
    (f has_integral i) s ∧ (g has_integral j) s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    i ≤ j

⊢ ∀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

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i

⊢ ∀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)])

⊢ ∀a b c.
    ((λx. c) has_integral content (interval [(a,b)]) * c)
      (interval [(a,b)])

⊢ ∀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)

⊢ ∀f g s i j.
    (f has_integral i) s ∧ (g has_integral j) s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    i ≤ j

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ i ≤ 0

⊢ ∀f s i. (f has_integral i) s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ i

⊢ ∀f s t i.
    (f has_integral i) s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
    0 ≤ i

⊢ ∀f. (f has_integral 0) ∅

⊢ ∀f i. (f has_integral i) ∅ ⇔ i = 0

⊢ ∀f g k s.
    (∀x. x ∈ s ⇒ f x = g x) ∧ (f has_integral k) s ⇒ (g has_integral k) s

⊢ ∀f g k s.
    (∀x. x ∈ s ⇒ f x = g x) ⇒ ((f has_integral k) s ⇔ (g has_integral k) s)

⊢ ∀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)])

⊢ ∀f i s. (f has_integral i) s ⇒ f integrable_on s

⊢ ∀f i s. (f has_integral i) s ⇔ f integrable_on s ∧ integral s f = i

⊢ ∀f s. f integrable_on s ⇔ (f has_integral integral s f) s

⊢ ∀f y s.
    negligible (frontier s) ⇒
    ((f has_integral y) (interior s) ⇔ (f has_integral y) s)

⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ (f has_integral 0) s

⊢ ∀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

⊢ ∀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

⊢ ∀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}

⊢ ∀f y s h. (f has_integral y) s ∧ linear h ⇒ (h ∘ f has_integral h y) s

⊢ ∀f s l.
    ((λx. f x * indicator s x) has_integral l) 𝕌(:real) ⇔
    (f has_integral l) s

⊢ ∀f k s. (f has_integral k) s ⇒ ((λx. -f x) has_integral -k) s

⊢ ∀f s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ f x = 0) ⇒ (f has_integral 0) t

⊢ ∀f s.
    (∀x i. x ∈ s ⇒ 0 ≤ f x) ⇒
    ((f has_integral 0) s ⇔ negligible {x | x ∈ s ∧ f x ≠ 0})

⊢ ∀f a b.
    content (interval [(a,b)]) = 0 ⇒ (f has_integral 0) (interval [(a,b)])

⊢ ∀f a b i.
    content (interval [(a,b)]) = 0 ⇒
    ((f has_integral i) (interval [(a,b)]) ⇔ i = 0)

⊢ ∀f s t i.
    (∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ (f has_integral i) s ⇒
    (f has_integral i) t

⊢ ∀f a. (f has_integral 0) (interval [(a,a)])

⊢ ∀f i a b.
    ((λx. f (-x)) has_integral i) (interval [(-b,-a)]) ⇔
    (f has_integral i) (interval [(a,b)])

⊢ ∀f i s.
    ((λx. f (-x)) has_integral i) s ⇔ (f has_integral i) (IMAGE (λx. -x) s)

⊢ ∀f i a b.
    (f has_integral i) (interval [(a,b)]) ⇒
    ((λx. f (-x)) has_integral i) (interval [(-b,-a)])

⊢ ∀f s t i.
    s ⊆ t ⇒
    (((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
     (f has_integral i) s)

⊢ ∀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)])

⊢ ∀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)]))

⊢ ∀f s t.
    ((λx. if x ∈ s then f x else 0) has_integral i) t ⇔
    (f has_integral i) (s ∩ t)

⊢ ∀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)])

⊢ ∀f s i.
    ((λx. if x ∈ s then f x else 0) has_integral i) 𝕌(:real) ⇔
    (f has_integral i) s

⊢ ∀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

⊢ ∀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

⊢ ∀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)

⊢ ∀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

⊢ ∀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)

⊢ ∀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)])

⊢ ∀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)]))

⊢ ∀f s t y.
    negligible (s DIFF t ∪ (t DIFF s)) ∧ (f has_integral y) s ⇒
    (f has_integral y) t

⊢ ∀f s t y.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒
    ((f has_integral y) s ⇔ (f has_integral y) t)

⊢ ∀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)])

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ∧ (g has_integral 0) s ⇒
    (f has_integral 0) s

⊢ ∀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)]))

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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)]))

⊢ ∀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)

⊢ ∀f i k1 k2. (f has_integral k1) i ∧ (f has_integral k2) i ⇒ k1 = k2

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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)]

⊢ ∀f s.
    bounded (IMAGE f s) ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≤ y ⇒ f x ≤ f y) ⇒
    f has_bounded_variation_on s

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    (λx. integral (interval [(x,b)]) f) continuous_on interval [(a,b)]

⊢ ∀f a b.
    f integrable_on interval [(a,b)] ⇒
    (λx. integral (interval [(a,x)]) f) continuous_on interval [(a,b)]

⊢ ∀s. (λx. 0) integrable_on s

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒ (λx. f x + g x) integrable_on s

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀f a b.
    f has_bounded_variation_on interval [(a,b)] ⇒
    f integrable_on interval [(a,b)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀f c s. f integrable_on s ⇒ (λx. c * f x) integrable_on s

⊢ ∀f s c. (λx. c * f x) integrable_on s ⇔ c = 0 ∨ f integrable_on s

⊢ ∀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)]

⊢ ∀f d s.
    d division_of s ∧ (∀i. i ∈ d ⇒ f integrable_on i) ⇒ f integrable_on s

⊢ ∀f s. f integrable_on s ⇔ (λx. f x) integrable_on s

⊢ ∀a b c. (λx. c) integrable_on interval [(a,b)]

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒ f integrable_on interval [(a,b)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)

⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ∧ f integrable_on s ⇒ g integrable_on s

⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ (f integrable_on s ⇔ g integrable_on s)

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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)

⊢ ∀f i. f integrable_on i ⇒ (f has_integral integral i f) i

⊢ ∀f h s. f integrable_on s ∧ linear h ⇒ h ∘ f integrable_on s

⊢ ∀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

⊢ ∀f s.
    (λx. f x * indicator s x) integrable_on 𝕌(:real) ⇔ f integrable_on s

⊢ ∀f s. f integrable_on s ⇒ (λx. -f x) integrable_on s

⊢ ∀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

⊢ ∀f. f integrable_on ∅

⊢ ∀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)]

⊢ ∀f a b. content (interval [(a,b)]) = 0 ⇒ f integrable_on interval [(a,b)]

⊢ ∀f a. f integrable_on interval [(a,a)]

⊢ ∀f s d i. d division_of i ∧ f integrable_on s ∧ i ⊆ s ⇒ f integrable_on i

⊢ ∀f s a b.
    f integrable_on s ∧ interval [(a,b)] ⊆ s ⇒
    f integrable_on interval [(a,b)]

⊢ ∀f s t.
    (∀x. x ∉ s ⇒ f x = 0) ∧ s ⊆ t ∧ f integrable_on s ⇒ f integrable_on t

⊢ ∀f a b.
    (λx. f (-x)) integrable_on interval [(-b,-a)] ⇔
    f integrable_on interval [(a,b)]

⊢ ∀f s. (λx. f (-x)) integrable_on s ⇔ f integrable_on IMAGE (λx. -x) s

⊢ ∀f s t.
    s ⊆ t ⇒
    ((λx. if x ∈ s then f x else 0) integrable_on t ⇔ f integrable_on s)

⊢ ∀f s t.
    (λx. if x ∈ s then f x else 0) integrable_on t ⇔ f integrable_on s ∩ t

⊢ ∀f s.
    (λx. if x ∈ s then f x else 0) integrable_on 𝕌(:real) ⇔
    f integrable_on s

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
    f integrable_on t ⇒
    g integrable_on t

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
    (f integrable_on t ⇔ g integrable_on t)

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
    f integrable_on t ⇒
    g integrable_on t

⊢ ∀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)]

⊢ ∀f s t.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒
    f integrable_on s ⇒
    f integrable_on t

⊢ ∀f s t.
    negligible (s DIFF t ∪ (t DIFF s)) ⇒
    (f integrable_on s ⇔ f integrable_on t)

⊢ ∀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}

⊢ ∀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

⊢ ∀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)]

⊢ ∀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)])

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒ (λx. f x − g x) integrable_on s

⊢ ∀f a b c d.
    f integrable_on interval [(a,b)] ∧ interval [(c,d)] ⊆ interval [(a,b)] ⇒
    f integrable_on interval [(c,d)]

⊢ ∀f s t.
    FINITE t ∧ (∀a. a ∈ t ⇒ f a integrable_on s) ⇒
    (λx. sum t (λa. f a x)) integrable_on s

⊢ ∀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)]

⊢ ∀s. integral s (λx. 0) = 0

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒
    integral s (λx. f x + g x) = integral s f + integral s g

⊢ ∀f c s. f integrable_on s ⇒ integral s (λx. c * f x) = c * integral s f

⊢ ∀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

⊢ ∀f d s.
    d division_of s ∧ (∀k. k ∈ d ⇒ f integrable_on k) ⇒
    integral s f = sum d (λi. integral i f)

⊢ ∀f d s.
    f integrable_on s ∧ d division_of s ⇒
    integral s f = sum d (λi. integral i f)

⊢ ∀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)

⊢ ∀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)

⊢ ∀f s. f integrable_on s ⇒ integral s f = integral s (λx. f x)

⊢ ∀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

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    integral s f ≤ integral s g

⊢ ∀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

⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f

⊢ ∀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)])

⊢ ∀a b c.
    integral (interval [(a,b)]) (λx. c) = content (interval [(a,b)]) * c

⊢ ∀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

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒
    integral s f ≤ integral s g

⊢ ∀f s. f integrable_on s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ integral s f

⊢ ∀f s t.
    f integrable_on s ∧ negligible t ∧ (∀x. x ∈ s DIFF t ⇒ 0 ≤ f x) ⇒
    0 ≤ integral s f

⊢ ∀f. integral ∅ f = 0

⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ integral s f = integral s g

⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ integral s f = 0

⊢ ∀s f y. f integrable_on s ⇒ (integral s f = y ⇔ (f has_integral y) s)

⊢ ∀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)])

⊢ ∀f a b.
    f continuous_on interval [(a,b)] ⇒
    ∀x. x ∈ interval [(a,b)] ⇒
        ((λu. integral (interval [(u,b)]) f) has_vector_derivative -f x)
          (at x within interval [(a,b)])

⊢ ∀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 [(u,b)]) f) has_vector_derivative -f x)
      (at x within interval [(a,b)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀f s h.
    f integrable_on s ∧ linear h ⇒ integral s (h ∘ f) = h (integral s f)

⊢ ∀f s. integral 𝕌(:real) (λx. f x * indicator s x) = integral s f

⊢ ∀f s. f integrable_on s ⇒ integral s (λx. -f x) = -integral s f

⊢ ∀f a b.
    content (interval [(a,b)]) = 0 ⇒ integral (interval [(a,b)]) f = 0

⊢ ∀f a. integral (interval [(a,a)]) f = 0

⊢ ∀f a b.
    integral (interval [(-b,-a)]) (λx. f (-x)) =
    integral (interval [(a,b)]) f

⊢ ∀f s. integral s (λx. f (-x)) = integral (IMAGE (λx. -x) s) f

⊢ ∀f s t. s ⊆ t ⇒ integral t (λx. if x ∈ s then f x else 0) = integral s f

⊢ ∀f s t. integral t (λx. if x ∈ s then f x else 0) = integral (s ∩ t) f

⊢ ∀f s. integral 𝕌(:real) (λx. if x ∈ s then f x else 0) = integral s f

⊢ ∀f g s t.
    negligible s ∧ (∀x. x ∈ t DIFF s ⇒ g x = f x) ⇒
    integral t f = integral t g

⊢ ∀f s t. negligible (s DIFF t ∪ (t DIFF s)) ⇒ integral s f = integral t f

⊢ ∀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

⊢ ∀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

⊢ ∀f g s.
    f integrable_on s ∧ g integrable_on s ⇒
    integral s (λx. f x − g x) = integral s f − integral s g

⊢ ∀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

⊢ ∀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

⊢ ∀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))

⊢ ∀f s t.
    f integrable_on s ∧ f integrable_on t ∧ negligible (s ∩ t) ⇒
    integral (s ∪ t) f = integral s f + integral t f

⊢ ∀f y k. (f has_integral y) k ⇒ integral k f = y

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀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)])

⊢ ∀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

⊢ ∀e a b c.
    interval [(a,b)] ∩ {x | abs (x − c) ≤ e} =
    interval [(max a (c − e),min b (c + e))]

⊢ ∀a b m c. ∃u v.
    IMAGE (λx. m * x + c) (interval [(a,b)]) = interval [(u,v)]

⊢ ∀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)]

⊢ ∀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)]

⊢ ∀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) = ∅

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀s. negligible s ⇔ ∀t. (indicator s has_integral 0) t

⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ negligible t) ⇒ negligible (BIGUNION s)

⊢ ∀s. negligible s ⇔ ∀t. bounded t ∧ t ⊆ s ⇒ negligible t

⊢ ∀s. countable s ⇒ negligible s

⊢ ∀s. (∀n. negligible (s n)) ⇒ negligible (BIGUNION {s n | n ∈ 𝕌(:num)})

⊢ ∀s t. negligible s ⇒ negligible (s DIFF t)

⊢ negligible ∅

⊢ ∀s. FINITE s ⇒ negligible s

⊢ ∀a b. negligible (interval [(a,b)] DIFF interval (a,b))

⊢ ∀a s. negligible (a INSERT s) ⇔ negligible s

⊢ ∀s t. negligible s ∨ negligible t ⇒ negligible (s ∩ t)

⊢ ∀s. negligible s ⇔ ∀n. negligible (s ∩ interval [(-n,n)])

⊢ ∀s. negligible s ⇔ ∀a b. negligible (s ∩ interval [(a,b)])

⊢ ∀s. negligible s ⇔ (indicator s has_integral 0) 𝕌(:real)

⊢ ∀a. negligible {a}

⊢ ∀c. negligible {x | x = c}

⊢ ∀s t. negligible s ∧ t ⊆ s ⇒ negligible t

⊢ ∀s t. negligible s ∧ negligible t ⇒ negligible (s ∪ t)

⊢ ∀s t. negligible (s ∪ t) ⇔ negligible s ∧ negligible t

⊢ ∀f s.
    (∀x i. x ∈ s ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
    f absolutely_integrable_on s

⊢ ∀f s t.
    negligible t ∧ (∀x i. x ∈ s DIFF t ⇒ 0 ≤ f x) ∧ f integrable_on s ⇒
    f absolutely_integrable_on s

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀f e.
    0 ≤ e ⇒
    operative $/\
      (λi. ∃g. (∀x. x ∈ i ⇒ abs (f x − g x) ≤ e) ∧ g integrable_on i)

⊢ operative $+ content

⊢ ∀op d a b f.
    monoidal op ∧ operative op f ∧ d division_of interval [(a,b)] ⇒
    iterate op d f = f (interval [(a,b)])

⊢ ∀P d a b.
    operative $/\ P ∧ d division_of interval [(a,b)] ⇒
    ((∀i. i ∈ d ⇒ P i) ⇔ P (interval [(a,b)]))

⊢ ∀op f. operative op f ⇒ f ∅ = neutral op

⊢ ∀f. operative $+
        (λk. f (interval_upperbound k) − f (interval_lowerbound k))

⊢ ∀f. operative $/\ (λi. f integrable_on i)

⊢ ∀f. operative (lifted $+)
        (λi. if f integrable_on i then SOME (integral i f) else NONE)

⊢ ∀f. operative $+ f ⇒
      operative (lifted $+)
        (λi.
             if f has_bounded_setvariation_on i then
               SOME (set_variation i f)
             else NONE)

⊢ ∀f. operative (lifted $+)
        (λi.
             if f has_bounded_variation_on i then
               SOME (vector_variation i f)
             else NONE)

⊢ ∀f. operative $+
        (λk. f (interval_upperbound k) − f (interval_lowerbound k))

⊢ ∀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)])

⊢ ∀op f a b.
    operative op f ∧ content (interval [(a,b)]) = 0 ⇒
    f (interval [(a,b)]) = neutral op

⊢ ∀p q s t.
    p division_of s ∧ q division_of t ∧ s ⊆ t ⇒ ∃r. p ⊆ r ∧ r division_of t

⊢ ∀a b c d.
    interval [(c,d)] ⊆ interval [(a,b)] ∧ interval [(c,d)] ≠ ∅ ⇒
    ∃p. p division_of interval [(a,b)] ∧ interval [(c,d)] ∈ p

⊢ ∀p a b.
    p division_of BIGUNION p ∧ BIGUNION p ⊆ interval [(a,b)] ⇒
    ∃q. p ⊆ q ∧ q division_of interval [(a,b)]

⊢ ∀s i.
    s tagged_partial_division_of i ⇒
    IMAGE SND s division_of BIGUNION (IMAGE SND s)

⊢ ∀P. (∀a b. content (interval [(a,b)]) = 0 ⇒ P (interval [(a,b)])) ⇒ P ∅

⊢ ∀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)])

⊢ ∀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)

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀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)])

⊢ ∀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)])

⊢ ∀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

⊢ ∀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)])

⊢ ∀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

⊢ ∀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

⊢ ∀s. set_variation s (λx. 0) = 0

⊢ ∀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

⊢ ∀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)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀f s t.
    f has_bounded_setvariation_on s ∧ t ⊆ s ⇒
    set_variation t f ≤ set_variation s f

⊢ ∀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

⊢ ∀f s.
    (∃d. d division_of s) ⇒
    set_variation s f = sup {sum d (λk. abs (f k)) | d division_of s}

⊢ ∀f a b.
    set_variation (interval [(a,b)]) f =
    sup {sum d (λk. abs (f k)) | d division_of interval [(a,b)]}

⊢ ∀f s.
    (∀a b. content (interval [(a,b)]) = 0 ⇒ f (interval [(a,b)]) = 0) ∧
    content s = 0 ∧ bounded s ⇒
    set_variation s f = 0

⊢ ∀f s. f has_bounded_setvariation_on s ⇒ 0 ≤ set_variation s f

⊢ ∀f s.
    set_variation (IMAGE (λx. -x) s) (λk. f (IMAGE (λx. -x) k)) =
    set_variation s f

⊢ ∀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))

⊢ ∀a f s.
    set_variation (IMAGE (λx. -a + x) s) (λk. f (IMAGE (λx. a + x) k)) =
    set_variation s f

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀d s a b.
    d division_of s ∧ s ⊆ interval [(a,b)] ⇒
    sum d content ≤ content (interval [(a,b)])

⊢ ∀f p e.
    FINITE p ∧ (∀q. q ⊆ p ⇒ abs (sum q f) ≤ e) ⇒
    sum p (λx. abs (f x)) ≤ 2 * 1 * e

⊢ ∀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)])

⊢ ∀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

⊢ ∀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)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀p s.
    p tagged_division_of s ⇔
    p tagged_partial_division_of s ∧ ∀x. x ∈ s ⇒ ∃t k. (t,k) ∈ p ∧ x ∈ k

⊢ ∀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 ∅

⊢ ∀s i. s tagged_division_of i ⇒ FINITE s

⊢ ∀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)]

⊢ ∀x a b.
    x ∈ interval [(a,b)] ⇒
    {(x,interval [(a,b)])} tagged_division_of interval [(a,b)]

⊢ ∀p. p tagged_division_of ∅ ⇔ p = ∅

⊢ ∀p s.
    p tagged_division_of s ⇒ p tagged_division_of BIGUNION (IMAGE SND p)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀p s. p tagged_division_of s ⇒ s = BIGUNION (IMAGE SND p)

⊢ ∀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)]

⊢ ∀p s y.
    p tagged_partial_division_of s ⇒
    CARD {(x,k) | (x,k) ∈ p ∧ y ∈ k ∧ content k ≠ 0} ≤ 2 ** 1

⊢ ∀p s x.
    p tagged_partial_division_of s ⇒
    CARD {(x,k) | k | (x,k) ∈ p ∧ content k ≠ 0} ≤ 2 ** 1

⊢ ∀p s t.
    p tagged_partial_division_of s ∧ s ⊆ t ⇒ p tagged_partial_division_of t

⊢ ∀p. p tagged_partial_division_of ∅ ⇔ p = ∅

⊢ ∀p s.
    p tagged_partial_division_of s ⇒
    p tagged_division_of BIGUNION (IMAGE SND p)

⊢ ∀s t i.
    s tagged_partial_division_of i ∧ t ⊆ s ⇒ t tagged_partial_division_of i

⊢ ∀p i k. p tagged_division_of i ∧ (x,k) ∈ p ⇒ x ∈ i

⊢ ∀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

⊢ ∀f s.
    (λx. f x) has_bounded_variation_on s ⇒
    vector_variation s (λx. abs (f x)) ≤ vector_variation s (λx. f x)

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀s c. vector_variation s (λx. c) = 0

⊢ ∀f s.
    is_interval s ∧ f has_bounded_variation_on s ⇒
    (vector_variation s f = 0 ⇔ ∃c. ∀x. x ∈ s ⇒ f x = c)

⊢ ∀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)]))

⊢ ∀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)]))

⊢ ∀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)]))

⊢ ∀f g s.
    (∀x. x ∈ s ⇒ f x = g x) ⇒ vector_variation s f = vector_variation s g

⊢ ∀f s a b.
    f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
    abs (f b − f a) ≤ vector_variation s f

⊢ ∀f s a b.
    f has_bounded_variation_on s ∧ segment [(a,b)] ⊆ s ⇒
    f b − f a ≤ vector_variation s f

⊢ ∀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)

⊢ ∀f s t.
    f has_bounded_variation_on s ∧ t ⊆ s ⇒
    vector_variation t f ≤ vector_variation s f

⊢ ∀f s. vector_variation s (λx. -f x) = vector_variation s f

⊢ ∀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

⊢ ∀f s. content s = 0 ∧ bounded s ⇒ vector_variation s f = 0

⊢ ∀f s. f has_bounded_variation_on s ⇒ 0 ≤ vector_variation s f

⊢ ∀f s.
    vector_variation s (λx. f (-x)) = vector_variation (IMAGE (λx. -x) s) f

⊢ ∀f s.
    vector_variation (IMAGE (λx. -x) s) (λx. f (-x)) = vector_variation s f

⊢ ∀f u v.
    vector_variation (interval [(u,v)]) (λx. f (-x)) =
    vector_variation (interval [(-v,-u)]) f

⊢ ∀a f s.
    vector_variation s (λx. f (a + x)) =
    vector_variation (IMAGE (λx. a + x) s) f

⊢ ∀a f s.
    vector_variation (IMAGE (λx. -a + x) s) (λx. f (a + x)) =
    vector_variation s f

⊢ ∀a f u v.
    vector_variation (interval [(u,v)]) (λx. f (a + x)) =
    vector_variation (interval [(a + u,a + v)]) f

⊢ ∀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

⊢ ∀f y a b.
    (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

⊢ ∀f i y.
    (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