Theory real_sigma

⊢ ∀f s. ∏ f s = ITSET (λe acc. f e * acc) s 1

⊢ ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0

⊢ concave_fn = {f | (λx. -f x) ∈ convex_fn}

⊢ convex_fn =
  {f |
   ∀x y t.
     0 ≤ t ∧ t ≤ 1 ⇒ f (t * x + (1 − t) * y) ≤ t * f x + (1 − t) * f y}

⊢ ∀s. indicator s = (λx. if x ∈ s then 1 else 0)

⊢ ∀p. polynomial_function p ⇔
      ∃m c. ∀x. p x = sum {0 .. m} (λi. c i * x pow i)

⊢ pos_concave_fn = {f | (λx. -f x) ∈ pos_convex_fn}

⊢ pos_convex_fn =
  {f |
   ∀x y t.
     0 < x ∧ 0 < y ∧ 0 ≤ t ∧ t ≤ 1 ⇒
     f (t * x + (1 − t) * y) ≤ t * f x + (1 − t) * f y}

⊢ product = iterate $*

⊢ sum = iterate $+

⊢ ∀s x. abs (indicator s x) = indicator s x

⊢ ∀x. abs x ≤ 0 ⇔ x = 0

⊢ ∀x y. abs (x * y) ≤ 1 / 2 * (x² + y²)

⊢ ∀s. FINITE s ⇒ &CARD s = sum s (λx. 1)

⊢ ∀s x. indicator s x = if x ∈ s then 1 else 0

⊢ ∀s x. abs (indicator s x) ≤ 1

⊢ ∀s x. indicator s x ≤ 1

⊢ ∀s x. 0 ≤ indicator s x

⊢ (∀a. INFINITE {x | a < x}) ∧ (∀a. INFINITE {x | a ≤ x}) ∧
  (∀b. INFINITE {x | x < b}) ∧ (∀b. INFINITE {x | x ≤ b}) ∧
  (∀a b. FINITE {x | a < x ∧ x < b} ⇔ b ≤ a) ∧
  (∀a b. FINITE {x | a ≤ x ∧ x < b} ⇔ b ≤ a) ∧
  (∀a b. FINITE {x | a < x ∧ x ≤ b} ⇔ b ≤ a) ∧
  ∀a b. FINITE {x | a ≤ x ∧ x ≤ b} ⇔ b ≤ a

⊢ ∀s. indicator (𝕌(:α) DIFF s) = (λx. 1 − indicator s x)

⊢ indicator ∅ = (λx. 0)

⊢ ∀s t x. s ⊆ t ⇒ indicator s x ≤ indicator t x

⊢ ∀s x. 0 ≤ indicator s x

⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
      (∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s

⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e

⊢ ∀s t.
    s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ∧ t ≠ ∅ ∧ (∃b. ∀x. x ∈ t ⇒ b ≤ x) ∧
    (∀a. (∀x. x ∈ s ⇒ a ≤ x) ⇔ ∀x. x ∈ t ⇒ a ≤ x) ⇒
    inf s = inf t

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ inf s ∈ s ∧ ∀x. x ∈ s ⇒ inf s ≤ x

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ b ≤ x

⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z

⊢ ∀x s. FINITE s ⇒ inf (x INSERT s) = if s = ∅ then x else min x (inf s)

⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r

⊢ ∀a. inf {a} = a

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ a ≤ y)

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

⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p

⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x

⊢ monoidal $+

⊢ monoidal $*

⊢ ∀f s s'.
    FINITE s ∧ FINITE s' ⇒
    SIGMA (λx. SIGMA (f x) s') s = SIGMA (λx. SIGMA (λy. f y x) s) s'

⊢ neutral $+ = 0

⊢ neutral $* = 1

⊢ ∀p n i. p permutes {1 .. n} ∧ i ∈ {1 .. n} ⇒ 1 ≤ p i ∧ p i ≤ n

⊢ ∀p q.
    polynomial_function p ∧ polynomial_function q ⇒
    polynomial_function (λx. p x + q x)

⊢ ∀c. polynomial_function (λx. c)

⊢ ∀p a. polynomial_function p ⇒ (FINITE {x | p x = a} ⇔ ¬∀x. p x = a)

⊢ polynomial_function (λx. x)

⊢ ∀P. P (λx. x) ∧ (∀c. P (λx. c)) ∧ (∀p q. P p ∧ P q ⇒ P (λx. p x + q x)) ∧
      (∀p q. P p ∧ P q ⇒ P (λx. p x * q x)) ⇒
      ∀p. polynomial_function p ⇒ P p

⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. c * p x)

⊢ ∀p q.
    polynomial_function p ∧ polynomial_function q ⇒
    polynomial_function (λx. p x * q x)

⊢ ∀p. polynomial_function (λx. -p x) ⇔ polynomial_function p

⊢ ∀p n. polynomial_function p ⇒ polynomial_function (λx. p x pow n)

⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. p x * c)

⊢ ∀p q.
    polynomial_function p ∧ polynomial_function q ⇒
    polynomial_function (λx. p x − q x)

⊢ ∀s p.
    FINITE s ∧ (∀i. i ∈ s ⇒ polynomial_function (λx. p x i)) ⇒
    polynomial_function (λx. sum s (p x))

⊢ ∀p q.
    polynomial_function p ∧ polynomial_function q ⇒
    polynomial_function (p ∘ q)

⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)

⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)

⊢ ∀f s. FINITE s ⇒ product s (λx. abs (f x)) = abs (product s f)

⊢ ∀f m n p.
    m ≤ n + 1 ⇒
    product {m .. n + p} f =
    product {m .. n} f * product {n + 1 .. n + p} f

⊢ (∀f. product ∅ f = 1) ∧
  ∀x f s.
    FINITE s ⇒
    product (x INSERT s) f =
    if x ∈ s then product s f else f x * product s f

⊢ ∀f m n. m ≤ n ⇒ product {m .. n} f = f m * product {m + 1 .. n} f

⊢ (∀m. product {m .. 0} f = if m = 0 then f 0 else 1) ∧
  ∀m n.
    product {m .. SUC n} f =
    if m ≤ SUC n then product {m .. n} f * f (SUC n)
    else product {m .. n} f

⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ product {m .. n} f = product {m .. n − 1} f * f n

⊢ ∀P f s.
    P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
    P (product s f)

⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ product s (λi. f i) = product s g) ∧
  (∀f g a b.
     (∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
     product {a .. b} (λi. f i) = product {a .. b} g) ∧
  ∀f g p.
    (∀x. p x ⇒ f x = g x) ⇒
    product {y | p y} (λi. f i) = product {y | p y} g

⊢ ∀c s. FINITE s ⇒ product s (λx. c) = c pow CARD s

⊢ ∀c m n. product {m .. n} (λx. c) = c pow (n + 1 − m)

⊢ ∀c n. product {1 .. n} (λx. c) = c pow n

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ f a * product (s DELETE a) f = product s f

⊢ ∀s a. product s (λx. if x = a then b else 1) = if a ∈ s then b else 1

⊢ ∀f g s. FINITE s ⇒ product s (λx. f x / g x) = product s f / product s g

⊢ ∀f g m n.
    product {m .. n} (λx. f x / g x) =
    product {m .. n} f / product {m .. n} g

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

⊢ ∀f s. FINITE s ⇒ (product s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)

⊢ ∀f n. product (count n) f = 0 ⇔ ∃i. i < n ∧ f i = 0

⊢ ∀f m n. product {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0

⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ product s f = 1

⊢ ∀f n. (∀i. i < n ⇒ f i = 1) ⇒ product (count n) f = 1

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ product {m .. n} f = 1

⊢ ∀f g n.
    (∀i. i < n ⇒ f i = g i) ⇒ product (count n) f = product (count n) g

⊢ ∀f g m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
    product {m .. n} f = product {m .. n} g

⊢ ∀f g s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    product (IMAGE f s) g = product s (g ∘ f)

⊢ ∀f s. FINITE s ⇒ product s (λx. (f x)⁻¹) = (product s f)⁻¹

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

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ 1) ⇒ product s f ≤ 1

⊢ ∀f m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
    product {m .. n} f ≤ product {m .. n} g

⊢ ∀f g s. FINITE s ⇒ product s (λx. f x * g x) = product s f * product s g

⊢ ∀f g n.
    product (count n) (λx. f x * g x) =
    product (count n) f * product (count n) g

⊢ ∀f g s.
    FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
    product s (λx. f x * g x) = product s f * product s g

⊢ ∀f g m n.
    product {m .. n} (λx. f x * g x) =
    product {m .. n} f * product {m .. n} g

⊢ ∀f s. FINITE s ⇒ product s (λi. -f i) = -1 pow CARD s * product s f

⊢ ∀f m n.
    product {m .. n} (λi. -f i) = -1 pow (n + 1 − m) * product {m .. n} f

⊢ ∀f n. product {1 .. n} (λi. -f i) = -1 pow n * product {1 .. n} f

⊢ ∀f m p. product {m + p .. n + p} f = product {m .. n} (λi. f (i + p))

⊢ ∀s. product s (λn. 1) = 1

⊢ ∀f m n.
    product {2 * m .. 2 * n + 1} f =
    product {m .. n} (λi. f (2 * i) * f (2 * i + 1))

⊢ ∀f p s. p permutes s ⇒ product s f = product s (f ∘ p)

⊢ ∀f p n.
    p permutes count n ⇒ product (count n) f = product (count n) (f ∘ p)

⊢ ∀f p m n.
    p permutes count n DIFF count m ⇒
    product (count n DIFF count m) f =
    product (count n DIFF count m) (f ∘ p)

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ product s f

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 ≤ f x) ⇒ 0 ≤ product {m .. n} f

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < product s f

⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < product {m .. n} f

⊢ ∀f x. product {x} f = f x

⊢ ∀f n. product {n .. n} f = f n

⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒ product v f = product u f

⊢ ∀f s. product (support $* f s) f = product s f

⊢ ∀f s t.
    FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
    product (s ∪ t) f = product s f * product t f

⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (inf s) ≤ a

⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (sup s) ≤ a

⊢ ∀x. 0 < x ⇒ ∃n. (&n)⁻¹ < x

⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x

⊢ ∀x k. -k < x ∧ x < k ⇔ abs x < k

⊢ ∀P. (∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇒
      ∃M. (∀x. P x ⇒ x ≤ M) ∧ ∀M'. (∀x. P x ⇒ x ≤ M') ⇒ M ≤ M'

⊢ ∀x y. abs x = abs y ⇔ x² = y²

⊢ (∀e. 0 < e / 2 ⇔ 0 < e) ∧ (∀e. e / 2 + e / 2 = e) ∧ ∀e. 2 * (e / 2) = e

⊢ ∀p x. (∃z. ∀r. r ∈ p ⇒ r ≤ z) ∧ (∃r. r ∈ p ∧ x ≤ r) ⇒ x ≤ sup p

⊢ ∀p x. (∃r. r ∈ p) ∧ (∀r. r ∈ p ⇒ r ≤ x) ⇒ sup p ≤ x

⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (inf s − l) ≤ e

⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ inf s ∧ inf s ≤ b

⊢ ∀p x.
    (∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ y ≤ z) ⇒
    (inf p ≤ x ⇔ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x)

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s ≤ a ⇔ ∃x. x ∈ s ∧ x ≤ a)

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s < a ⇔ ∃x. x ∈ s ∧ x < a)

⊢ ∀s b.
    (∀x. x ∈ s ⇒ b ≤ x) ∧ (∀b'. b < b' ⇒ ∃x. x ∈ s ∧ x < b') ⇒ inf s = b

⊢ ∀a b. a ≤ b ⇔ ∃x. a ≤ x ∧ x ≤ b

⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ inf s ⇔ ∀x. x ∈ s ⇒ a ≤ x)

⊢ ∀s t. t ≠ ∅ ∧ t ⊆ s ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒ inf s ≤ inf t

⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x ≤ z / y ⇔ y ≤ x)

⊢ ∀x y z. z < 0 ⇒ (x ≤ y / z ⇔ y ≤ x * z)

⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y

⊢ ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y

⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y

⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)

⊢ ∀x y. abs x ≤ abs y ⇔ x² ≤ y²

⊢ ∀s a b y. y ∈ s ∧ a ≤ y ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ sup s

⊢ ∀p x.
    (∃y. y ∈ p) ∧ (∃y. ∀z. z ∈ p ⇒ z ≤ y) ⇒
    (x ≤ sup p ⇔ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y)

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ sup s ⇔ ∃x. x ∈ s ∧ a ≤ x)

⊢ ∀a b. a < b ⇔ ∃x. a < x ∧ x < b

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < inf s ⇔ ∀x. x ∈ s ⇒ a < x)

⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹

⊢ ∀x y z. 0 < x ∧ x * y < x * z ⇒ y < z

⊢ ∀x y z. 0 < x ∧ 0 < y ∧ 0 < z ⇒ (z / x < z / y ⇔ y < x)

⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y

⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0

⊢ ∀x y z. x < 0 ⇒ (x * y < x * z ⇔ z < y)

⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0

⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y

⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d

⊢ ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y

⊢ ∀n. 0 < 2 pow n

⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)

⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0

⊢ ∀x y z. z < 0 ⇒ (x * z < y * z ⇔ y < x)

⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0

⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)

⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y

⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x

⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x

⊢ ∀r. r * r = r ⇔ r = 0 ∨ r = 1

⊢ ∀s t f g.
    FINITE s ∧ FINITE t ⇒
    sum s f * sum t g = sum s (λi. sum t (λj. f i * g j))

⊢ ∀f g m n p q.
    sum {m .. n} f * sum {p .. q} g =
    sum {m .. n} (λi. sum {p .. q} (λj. f i * g j))

⊢ ∀x. x < 0 ⇒ x ≠ 0

⊢ ∀m n. &m ≥ &n ⇔ m ≥ n

⊢ ∀f s. FINITE s ⇒ &nproduct s f = product s (λx. &f x)

⊢ ∀f s. FINITE s ⇒ &nsum s f = sum s (λx. &f x)

⊢ ∀f m n. &nsum {m .. n} f = sum {m .. n} (λi. &f i)

⊢ ∀n c.
    (∀x. sum {0 .. n} (λi. c i * x pow i) = 0) ⇔ ∀i. i ∈ {0 .. n} ⇒ c i = 0

⊢ ∀n c k.
    (∀x. sum {0 .. n} (λi. c i * x pow i) = k) ⇔
    c 0 = k ∧ ∀i. i ∈ {1 .. n} ⇒ c i = 0

⊢ ∀n c.
    FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ⇔
    ∃i. i ∈ {0 .. n} ∧ c i ≠ 0

⊢ ∀n c.
    ¬(∀i. i ∈ {0 .. n} ⇒ c i = 0) ⇒
    FINITE {x | sum {0 .. n} (λi. c i * x pow i) = 0} ∧
    CARD {x | sum {0 .. n} (λi. c i * x pow i) = 0} ≤ n

⊢ ∀f. ∏ f ∅ = 1

⊢ ∀f e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)

⊢ ∀f e. ∏ f {e} = f e

⊢ ∀f. ∏ f ∅ = 1 ∧
      ∀e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)

⊢ ∀a x y n.
    1 ≤ n ⇒
    sum {0 .. n} (λi. a i * x pow i) − sum {0 .. n} (λi. a i * y pow i) =
    (x − y) *
    sum {0 .. n − 1}
      (λj. sum {j + 1 .. n} (λi. a i * y pow (i − j − 1)) * x pow j)

⊢ ∀a x y n.
    1 ≤ n ⇒
    sum {0 .. n} (λi. a i * x pow i) − sum {0 .. n} (λi. a i * y pow i) =
    (x − y) *
    sum {0 .. n − 1}
      (λj. sum {0 .. n − j − 1} (λk. a (j + k + 1) * y pow k) * x pow j)

⊢ ∀x y n.
    1 ≤ n ⇒
    x pow n − y pow n =
    (x − y) * sum {0 .. n − 1} (λi. x pow i * y pow (n − 1 − i))

⊢ ∀x n. 1 ≤ n ⇒ 1 − x pow n = (1 − x) * sum {0 .. n − 1} (λi. x pow i)

⊢ ∀x n. 1 ≤ n ⇒ x pow n − 1 = (x − 1) * sum {0 .. n − 1} (λi. x pow i)

⊢ ∀s. FINITE s ⇒ SIGMA (λx. 0) s = 0

⊢ ∀f s. FINITE s ⇒ abs (SIGMA f s) ≤ SIGMA (abs ∘ f) s

⊢ ∀s. FINITE s ⇒ ∀f f'. SIGMA (λx. f x + f' x) s = SIGMA f s + SIGMA f' s

⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ SIGMA f s ≤ &CARD s * b

⊢ ∀P. FINITE P ⇒ ∀f c. SIGMA (λx. c * f x) P = c * SIGMA f P

⊢ ∀P. FINITE P ⇒
      ∀f. SIGMA f P = 1 ∧ (∀x y. x ∈ P ∧ y ∈ P ⇒ f x = f y) ⇒
          ∀x. x ∈ P ⇒ f x = (&CARD P)⁻¹

⊢ ∀f n. SIGMA f (count n) = sum (0,n) f

⊢ ∀f s1 s2.
    FINITE s1 ∧ FINITE s2 ⇒
    SIGMA (λ(x,y). f (x,y)) (s1 × s2) = SIGMA (λ(y,x). f (x,y)) (s2 × s1)

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ sum (s DELETE a) f = SIGMA f s − f a

⊢ ∀P P'.
    FINITE P ∧ FINITE P' ∧ DISJOINT P P' ⇒
    ∀f. SIGMA f (P ∪ P') = SIGMA f P + SIGMA f P'

⊢ ∀f. SIGMA f ∅ = 0

⊢ ∀s f f'. FINITE s ∧ (∀x. x ∈ s ⇒ f x = f' x) ⇒ SIGMA f s = SIGMA f' s

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = 0) ⇒ SIGMA f s = 0

⊢ ∀P. FINITE P ⇒ SIGMA (λx. if x ∈ P then 1 else 0) P = &CARD P

⊢ ∀n r. sum (0,n) r = SIGMA r (count n)

⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. f y = x) ⇒ SIGMA f P = &CARD P * x

⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. y ∈ P ⇒ f y = x) ⇒ SIGMA f P = &CARD P * x

⊢ ∀P. FINITE P ⇒ ∀c. SIGMA (λx. c) P = &CARD P * c

⊢ ∀P. FINITE P ⇒
      ∀f p. p ∈ P ∧ (∀q. q ∈ P ⇒ f p = f q) ⇒ SIGMA f P = &CARD P * f p

⊢ ∀s P f.
    FINITE s ∧ (∀x. x ∈ s ⇒ P x) ⇒
    SIGMA (λx. if P x then f x else 0) s = SIGMA f s

⊢ ∀P. FINITE P ⇒
      ∀f'.
        INJ f' P (IMAGE f' P) ⇒ ∀f. SIGMA f (IMAGE f' P) = SIGMA (f ∘ f') P

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
    SIGMA g (IMAGE f s) ≤ SIGMA (g ∘ f) s

⊢ ∀P. FINITE P ⇒
      ∀f P'. (∀x. x ∉ P' ⇒ f x = 0) ⇒ SIGMA f (P ∩ P') = SIGMA f P

⊢ ∀P. FINITE P ⇒ ∀f. SIGMA f (P ∩ (λp. f p ≠ 0)) = SIGMA f P

⊢ ∀P. P ≠ ∅ ∧ FINITE P ⇒ SIGMA (λs. if s ∈ P then (&CARD P)⁻¹ else 0) P = 1

⊢ ∀P. FINITE P ⇒ ∀f. SIGMA f P = SIGMA (λx. if x ∈ P then f x else 0) P

⊢ ∀s f z. FINITE s ⇒ SIGMA f s = SIGMA (λx. if x ∈ s then f x else z) s

⊢ ∀P. FINITE P ⇒ ∀f f'. (∀x. x ∈ P ⇒ f x ≤ f' x) ⇒ SIGMA f P ≤ SIGMA f' P

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
    SIGMA f s < SIGMA g s

⊢ ∀f s t.
    FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
    SIGMA f s ≤ SIGMA f t

⊢ ∀P. FINITE P ⇒ ∀f. SIGMA (λx. -f x) P = -SIGMA f P

⊢ ∀P. FINITE P ⇒
      ∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ∧ (∃x. x ∈ P ∧ f x ≠ 0) ⇒
          (SIGMA f P ≠ 0 ⇔ P ≠ ∅)

⊢ ∀f p s. FINITE s ∧ p PERMUTES s ⇒ SIGMA f s = SIGMA (f ∘ p) s

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ SIGMA f s

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒
    0 < SIGMA f s

⊢ ∀P. FINITE P ⇒ ∀f. (∀x. x ∈ P ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ P ⇒ f x ≤ SIGMA f P

⊢ ∀a s. FINITE s ⇒ (SIGMA a s)² = SIGMA (λ(i,j). a i * a j) (s × s)

⊢ ∀s s' f.
    FINITE s ∧ FINITE s' ⇒
    SIGMA (λx. SIGMA (f x) s') s = SIGMA (λx. f (FST x) (SND x)) (s × s')

⊢ ∀f e. SIGMA f {e} = f e

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀f. (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < SIGMA f s

⊢ ∀s f f'. FINITE s ⇒ SIGMA (λx. f x − f' x) s = SIGMA f s − SIGMA f' s

⊢ ∀f s t.
    FINITE s ∧ FINITE t ⇒
    SIGMA (λi. SIGMA (f i) t) s = SIGMA (λj. SIGMA (λi. f i j) s) t

⊢ ∀f. SIGMA f ∅ = 0 ∧
      ∀e s. FINITE s ⇒ SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e)

⊢ ∀f s. FINITE s ⇒ SIGMA f s = sum s f

⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (sup s − l) ≤ e

⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ sup s ∧ sup s ≤ b

⊢ ∀s. s ≠ ∅ ∧ (∃B. ∀x. x ∈ s ⇒ abs x ≤ B) ⇒ (sup s = inf s ⇔ ∃a. s = {a})

⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b

⊢ ∀s y. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒ (sup s ≤ y ⇔ ∀x. x ∈ s ⇒ x ≤ y)

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)

⊢ ∀s t. s ≠ ∅ ∧ s ⊆ t ∧ (∃b. ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s ≤ sup t

⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x

⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s < a ⇔ ∀x. x ∈ s ⇒ x < a)

⊢ ∀s b.
    (∀x. x ∈ s ⇒ x ≤ b) ∧ (∀b'. b' < b ⇒ ∃x. x ∈ s ∧ b' < x) ⇒ sup s = b

⊢ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x ≤ y ⇒ P x y) ⇒ ∀x y. P x y

⊢ (∀x. P x x) ∧ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x < y ⇒ P x y) ⇒ ∀x y. P x y

⊢ ∀P x. (∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P

⊢ ∀s t. {x + y | x ∈ s ∧ y ∈ t} = {y + x | y ∈ t ∧ x ∈ s}

⊢ ∀s. sum s (λn. 0) = 0

⊢ ∀f s. FINITE s ⇒ abs (sum s f) ≤ sum s (λx. abs (f x))

⊢ ∀s f b.
    FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ b) ⇒ abs (sum s f) ≤ &CARD s * b

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒ abs (sum s f) ≤ sum s g

⊢ ∀f m n. abs (sum {m .. n} f) ≤ sum {m .. n} (λi. abs (f i))

⊢ ∀s f b. FINITE s ∧ sum s (λa. abs (f a)) ≤ b ⇒ abs (sum s f) ≤ b

⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x + g x) = sum s f + sum s g

⊢ ∀f g n. sum (count n) (λx. f x + g x) = sum (count n) f + sum (count n) g

⊢ ∀f g s.
    FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
    sum s (λx. f x + g x) = sum s f + sum s g

⊢ ∀f g m n. sum {m .. n} (λi. f i + g i) = sum {m .. n} f + sum {m .. n} g

⊢ ∀f m n p.
    m ≤ n + 1 ⇒
    sum {m .. n + p} f = sum {m .. n} f + sum {n + 1 .. n + p} f

⊢ ∀f s.
    FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
    (∀t1 t2 x. t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ f x = 0) ⇒
    sum (BIGUNION s) f = sum s (λt. sum t f)

⊢ ∀f p s.
    (∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
    sum s f = sum s (f ∘ p)

⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ sum s f ≤ &CARD s * b

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b / &CARD s) ⇒ sum s f ≤ b

⊢ ∀s f b.
    FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
    sum s f < &CARD s * b

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ sum s f < &CARD s * b

⊢ ∀s f b. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b / &CARD s) ⇒ sum s f < b

⊢ ∀s P f g.
    FINITE s ⇒
    sum s (λx. if P x then f x else g x) =
    sum {x | x ∈ s ∧ P x} f + sum {x | x ∈ s ∧ ¬P x} g

⊢ ∀s a.
    FINITE s ∧ a ∈ s ⇒
    sum s (λx. if x = a then y else f x) = sum s f + (y − f a)

⊢ (∀f. sum ∅ f = 0) ∧
  ∀x f s.
    FINITE s ⇒
    sum (x INSERT s) f = if x ∈ s then sum s f else f x + sum s f

⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = f m + sum {m + 1 .. n} f

⊢ (∀m. sum {m .. 0} f = if m = 0 then f 0 else 0) ∧
  ∀m n.
    sum {m .. SUC n} f =
    if m ≤ SUC n then sum {m .. n} f + f (SUC n) else sum {m .. n} f

⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ sum {m .. n} f = sum {m .. n − 1} f + f n

⊢ ∀P f s.
    P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
    P (sum s f)

⊢ ∀f m n p.
    0 < n ∧ m ≤ n ∧ n ≤ p + 1 ⇒
    sum {m .. n − 1} f + sum {n .. p} f = sum {m .. p} f

⊢ ∀f m n p.
    m ≤ n + 1 ∧ n ≤ p ⇒
    sum {m .. n} f + sum {n + 1 .. p} f = sum {m .. p} f

⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ sum s (λi. f i) = sum s g) ∧
  (∀f g a b.
     (∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
     sum {a .. b} (λi. f i) = sum {a .. b} g) ∧
  ∀f g p. (∀x. p x ⇒ f x = g x) ⇒ sum {y | p y} (λi. f i) = sum {y | p y} g

⊢ ∀c s. FINITE s ⇒ sum s (λn. c) = &CARD s * c

⊢ ∀c m n. sum {m .. n} (λn. c) = &(n + 1 − m) * c

⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ sum s f = 0

⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ sum (s DELETE a) f = sum s f − f a

⊢ ∀f s a.
    FINITE s ⇒
    sum (s DELETE a) f = if a ∈ s then sum s f − f a else sum s f

⊢ ∀s a. sum s (λx. if x = a then b else 0) = if a ∈ s then b else 0

⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ sum (s DIFF t) f = sum s f − sum t f

⊢ ∀m n.
    sum {m .. n} (λk. f k − f (k + 1)) =
    if m ≤ n then f m − f (n + 1) else 0

⊢ ∀m n.
    sum {m .. n} (λk. f (k + 1) − f k) =
    if m ≤ n then f (n + 1) − f m else 0

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

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

⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0) ⇒ sum {m .. n} f = 0

⊢ ∀f g n. (∀i. i < n ⇒ f i = g i) ⇒ sum (count n) f = sum (count n) g

⊢ ∀s t f g h.
    (∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
    (∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
    sum s f = sum t g

⊢ ∀s t f g h k.
    (∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
    (∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
    sum s f = sum t g

⊢ ∀f g m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒ sum {m .. n} f = sum {m .. n} g

⊢ ∀f s t.
    FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ f x = g x) ∧
    (∀x. x ∈ s ∧ x ∉ t ⇒ f x = 0) ⇒
    sum s f = sum t g

⊢ ∀x m n.
    sum {m .. n} (λi. x pow i) =
    if n < m then 0
    else if x = 1 then &(n + 1 − m)
    else (x pow m − x pow SUC n) / (1 − x)

⊢ ∀x n. (1 − x) * sum {0 .. n} (λi. x pow i) = 1 − x pow SUC n

⊢ ∀x m n.
    m ≤ n ⇒ (1 − x) * sum {m .. n} (λi. x pow i) = x pow m − x pow SUC n

⊢ ∀f g s t.
    FINITE s ∧ IMAGE f s ⊆ t ⇒
    sum t (λy. sum {x | x ∈ s ∧ f x = y} g) = sum s g

⊢ ∀f g s.
    (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
    sum (IMAGE f s) g = sum s (g ∘ f)

⊢ ∀f g s.
    FINITE s ⇒ sum s g = sum (IMAGE f s) (λy. sum {x | x ∈ s ∧ f x = y} g)

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
    sum (IMAGE f s) g ≤ sum s (g ∘ f)

⊢ ∀d i s.
    FINITE s ∧ (∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ i x = i y ⇒ d (i x) = 0) ⇒
    sum (IMAGE i s) d = sum s (d ∘ i)

⊢ ∀s t f.
    FINITE s ∧ FINITE t ⇒ sum s f + sum t f = sum (s ∪ t) f + sum (s ∩ t) f

⊢ ∀f p s.
    FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
    (∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
    sum s (f ∘ p) = sum s f

⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ sum s f ≤ sum s g

⊢ ∀f g s t i.
    FINITE s ∧ FINITE t ∧ (∀y. y ∈ t ⇒ 0 ≤ g y) ∧
    (∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ i y = x ∧ f x ≤ g y) ⇒
    sum s f ≤ sum t g

⊢ ∀f g m n.
    (∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒ sum {m .. n} f ≤ sum {m .. n} g

⊢ ∀f c s. sum s (λx. c * f x) = c * sum s f

⊢ ∀f g s.
    FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
    sum s f < sum s g

⊢ ∀f g s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ sum s f < sum s g

⊢ ∀R s t k.
    FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k) ⇒
    sum s (λi. &CARD (equiv_class R t i)) = &(k * CARD t)

⊢ ∀R s t k.
    FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k j) ⇒
    sum s (λi. &CARD (equiv_class R t i)) = sum t (λi. &k i)

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

⊢ ∀p f m n. sum {m + p .. n + p} f = sum {m .. n} (λi. f (i + p))

⊢ ∀f m n. m ≤ n ⇒ sum {m .. n} f = sum {0 .. n − m} (λi. f (i + m))

⊢ ∀f m n.
    sum {2 * m .. 2 * n + 1} f =
    sum {m .. n} (λi. f (2 * i) + f (2 * i + 1))

⊢ ∀f g m n.
    sum {m .. n} (λk. f k * (g k − g (k − 1))) =
    if m ≤ n then
      f (n + 1) * g n − f m * g (m − 1) −
      sum {m .. n} (λk. g k * (f (k + 1) − f k))
    else 0

⊢ ∀f g m n.
    sum {m .. n} (λk. f k * (g (k + 1) − g k)) =
    if m ≤ n then
      f (n + 1) * g (n + 1) − f m * g m −
      sum {m .. n} (λk. g (k + 1) * (f (k + 1) − f k))
    else 0

⊢ ∀f s q.
    q permutes s ⇒
    sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (q ∘ p))

⊢ ∀f n q.
    q permutes count n ⇒
    sum {p | p permutes count n} f =
    sum {p | p permutes count n} (λp. f (q ∘ p))

⊢ ∀f m n q.
    q permutes count n DIFF count m ⇒
    sum {p | p permutes count n DIFF count m} f =
    sum {p | p permutes count n DIFF count m} (λp. f (q ∘ p))

⊢ ∀f s q.
    q permutes s ⇒
    sum {p | p permutes s} f = sum {p | p permutes s} (λp. f (p ∘ q))

⊢ ∀f n q.
    q permutes count n ⇒
    sum {p | p permutes count n} f =
    sum {p | p permutes count n} (λp. f (p ∘ q))

⊢ ∀f m n q.
    q permutes count n DIFF count m ⇒
    sum {p | p permutes count n DIFF count m} f =
    sum {p | p permutes count n DIFF count m} (λp. f (p ∘ q))

⊢ ∀f n.
    sum {p | p permutes count n} f =
    sum {p | p permutes count n} (λp. f (inverse p))

⊢ ∀f p s. p permutes s ⇒ sum s f = sum s (f ∘ p)

⊢ ∀f p n. p permutes count n ⇒ sum (count n) f = sum (count n) (f ∘ p)

⊢ ∀f p m n.
    p permutes count n DIFF count m ⇒
    sum (count n DIFF count m) f = sum (count n DIFF count m) (f ∘ p)

⊢ ∀f b s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f = 0 ⇒ ∀x. x ∈ s ⇒ f x = 0

⊢ ∀f m n.
    (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ∧ sum {m .. n} f = 0 ⇒
    ∀p. m ≤ p ∧ p ≤ n ⇒ f p = 0

⊢ ∀s. (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ sum s f

⊢ ∀m n f. (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ⇒ 0 ≤ sum {m .. n} f

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < sum s f

⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < sum s f

⊢ ∀f s. FINITE s ⇒ sum s (λx. if x ∈ s then f x else 0) = sum s f

⊢ ∀P s f. sum {x | x ∈ s ∧ P x} f = sum s (λx. if P x then f x else 0)

⊢ ∀f c s. sum s (λx. f x * c) = sum s f * c

⊢ ∀f x. sum {x} f = f x

⊢ ∀f n. sum {n .. n} f = f n

⊢ ∀f g s. FINITE s ⇒ sum s (λx. f x − g x) = sum s f − sum s g

⊢ ∀u v f.
    FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x ≤ 0) ∧
    (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
    sum u f ≤ sum v f

⊢ ∀u v f.
    FINITE v ∧ u ⊆ v ∧ (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒ sum u f ≤ sum v f

⊢ ∀f g m n. sum {m .. n} (λi. f i − g i) = sum {m .. n} f − sum {m .. n} g

⊢ ∀s t x.
    FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
    sum s (λi. sum (t i) (x i)) =
    sum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)

⊢ ∀R f s t.
    FINITE s ∧ FINITE t ⇒
    sum s (λx. sum (equiv_class R t x) (λy. f x y)) =
    sum t (λy. sum {x | x ∈ s ∧ R x y} (λx. f x y))

⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ sum v f = sum u f

⊢ ∀f s. sum (support $+ f s) f = sum s f

⊢ ∀f s t.
    FINITE s ∧ FINITE t ⇒
    sum s (λi. sum t (f i)) = sum t (λj. sum s (λi. f i j))

⊢ ∀f m n.
    sum (count m) (λi. sum (count n) (f i)) =
    sum (count n) (λj. sum (count m) (λi. f i j))

⊢ ∀a b c d f.
    sum {a .. b} (λi. sum {c .. d} (f i)) =
    sum {c .. d} (λj. sum {a .. b} (λi. f i j))

⊢ ∀f m n. n < m ⇒ sum {m .. n} f = 0

⊢ ∀f s t.
    FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒ sum (s ∪ t) f = sum s f + sum t f

⊢ ∀s t u. FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ sum s f + sum t f = sum u f

⊢ ∀f u v.
    FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ f x = 0) ⇒ sum (u ∪ v) f = sum v f

⊢ ∀f s t.
    FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = 0) ⇒
    sum (s ∪ t) f = sum s f + sum t f

⊢ ∀f u v.
    FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ sum (u ∪ v) f = sum u f

⊢ ∀u s.
    FINITE s ∧ sum s u = 0 ⇒
    (∀i. i ∈ s ⇒ u i = 0) ∨ ∃j k. j ∈ s ∧ u j < 0 ∧ k ∈ s ∧ u k > 0

⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
      (∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b

⊢ ∀s t. (∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇔ ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s = sup t

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b

⊢ ∀x s. FINITE s ⇒ sup (x INSERT s) = if s = ∅ then x else max x (sup s)

⊢ ∀p q.
    (∃b. ∀n. p n ≤ b) ∧ (∃c. ∀n. q n ≤ c) ∧ (∀n. p n ≤ q n) ⇒
    sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))

⊢ ∀a. sup {a} = a

⊢ ∀s t.
    s ≠ ∅ ∧ t ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ∧ (∃c. ∀x. x ∈ t ⇒ x ≤ c) ⇒
    sup (s ∪ t) = max (sup s) (sup t)

⊢ ∀s b. (∀c. (∀x. x ∈ s ⇒ x ≤ c) ⇔ b ≤ c) ⇒ sup s = b

⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ (sup s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)

⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a

⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
      inf s = @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a

⊢ ∀s. FINITE s ⇒
      ∀f g g'.
        SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧ f ∈ concave_fn ⇒
        SIGMA (λx. g x * f (g' x)) s ≤ f (SIGMA (λx. g x * g' x) s)

⊢ ∀s. FINITE s ⇒
      ∀f g g'.
        SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧ f ∈ convex_fn ⇒
        f (SIGMA (λx. g x * g' x) s) ≤ SIGMA (λx. g x * f (g' x)) s

⊢ ∀s. FINITE s ⇒
      ∀f g g'.
        SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
        (∀x. x ∈ s ⇒ 0 < g x ⇒ 0 < g' x) ∧ f ∈ pos_concave_fn ⇒
        SIGMA (λx. g x * f (g' x)) s ≤ f (SIGMA (λx. g x * g' x) s)

⊢ ∀s. FINITE s ⇒
      ∀f g g'.
        SIGMA g s = 1 ∧ (∀x. x ∈ s ⇒ 0 ≤ g x ∧ g x ≤ 1) ∧
        (∀x. x ∈ s ⇒ 0 < g x ⇒ 0 < g' x) ∧ f ∈ pos_convex_fn ⇒
        f (SIGMA (λx. g x * g' x) s) ≤ SIGMA (λx. g x * f (g' x)) s

⊢ INFINITE 𝕌(:real)

⊢ ∀f n. sum {0 .. n} f = sum (0,SUC n) f

⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b