Theory extreal

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

⊢ ∀top f.
    C_b top f ⇔ continuous_map (top,euclidean) f ∧ bounded (IMAGE f 𝕌(:α))

⊢ ∀s. ext_bounded s ⇔ ∃a. a ≠ +∞ ∧ ∀x. x ∈ s ⇒ abs x ≤ a

⊢ ∀f net. ext_continuous f net ⇔ (f ⟶ f (netlimit net)) net

⊢ ∀f s.
    ext_continuous_on f s ⇔ ∀x. x ∈ s ⇒ ext_continuous f (at x within s)

⊢ ext_euclidean = mtop extreal_mr1

⊢ ∀a. liminf a = sup (IMAGE (λm. inf {a n | m ≤ n}) 𝕌(:num))

⊢ ∀a. limsup a = inf (IMAGE (λm. sup {a n | m ≤ n}) 𝕌(:num))

⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m

⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n

⊢ ext_product = iterate $*

⊢ ∀f. (∀n. 0 ≤ f n) ⇒ suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))

⊢ $--> = limit ext_euclidean

⊢ (∀x. exp (Normal x) = Normal (exp x)) ∧ exp +∞ = +∞ ∧ exp −∞ = Normal 0

⊢ ∀p. inf p = -sup (IMAGE numeric_negate p)

⊢ ∀x. lg x = logr 2 x

⊢ ∀net f. lim net f = @l. (f ⟶ l) net

⊢ (∀x. 0 < x ⇒ ln (Normal x) = Normal (ln x)) ∧ ln (Normal 0) = −∞ ∧
  ln +∞ = +∞

⊢ (∀b x. logr b (Normal x) = Normal (logr b x)) ∧ ∀b. logr b +∞ = +∞

⊢ extreal_mr1 = metric (UNCURRY extreal_dist)

⊢ ∀x a. x powr a = exp (a * ln x)

⊢ ∀p. sup p =
      if ∀x. (∀y. p y ⇒ y ≤ x) ⇒ x = +∞ then +∞
      else if ∀x. p x ⇒ x = −∞ then −∞
      else Normal (sup (λr. p (Normal r)))

⊢ ∀a b f.
    (a,b) flat_area_of f ⇔
    a < b ∧
    ∃c. (∀x. a < x ∧ x < b ⇒ f x = c) ∧ (∀x. x < a ⇒ f x < c) ∧
        ∀x. b < x ⇒ c < f x

⊢ ∀f. flat_areas f = {open_interval a b | (a,b) flat_area_of f}

⊢ ∀f. flat_values f = IMAGE (sup ∘ IMAGE f) (flat_areas f)

⊢ ∀f. f⁻ = (λx. if f x < 0 then -f x else 0)

⊢ ∀f. f⁺ = (λx. if 0 < f x then f x else 0)

⊢ ∀s. 𝟙 s = Normal ∘ indicator s

⊢ ∀f. jumping_area f =
      {open_interval a b |
       ∃x0.
         x0 jumping_point_of f ∧ a = sup {f x | x < Normal x0} ∧
         b = inf {f x | Normal x0 < x}}

⊢ ∀x0 f.
    x0 jumping_point_of f ⇔
    sup {f x | x < Normal x0} ≠ inf {f x | Normal x0 < x}

⊢ (∀g x. max_fn_seq g 0 x = g 0 x) ∧
  ∀g n x. max_fn_seq g (SUC n) x = max (max_fn_seq g n x) (g (SUC n) x)

⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f x

⊢ ∀a b. open_interval a b = {x | a < x ∧ x < b}

⊢ open_intervals = {open_interval a b | T}

⊢ rational_intervals = {open_interval a b | a ∈ ℚ꙳ ∧ b ∈ ℚ꙳}

⊢ ∀f. right_continuous f ⇔
      (∀x y. x ≤ y ⇒ f x ≤ f y) ∧ ∀x. f right_continuous_at Normal x

⊢ ∀f x0. f right_continuous_at x0 ⇔ inf {f x | x0 < x} = f x0

⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
  ∀P n.
    seq_sup P (SUC n) =
    @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow SUC n) ∧ seq_sup P n < r ∧
        r < sup P

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

⊢ countable rational_intervals

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

⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x

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

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

⊢ ∀x. x ≠ +∞ ⇒ ∃n. x < 2 pow n

⊢ ∀e. 0 < e ⇒ ∃n. Normal ((1 / 2) pow n) < e

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y = x + z ⇔ y = z)

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x + z = y + z ⇔ x = y)

⊢ ∀f l net.
    (f ⟶ l) net ⇔
    trivial_limit net ∨
    ∀e. 0 < e ⇒
        ∃y. (∃x. netord net x y) ∧
            ∀x. netord net x y ⇒ dist extreal_mr1 (f x,l) < e

⊢ ∀net f g l m. (f ⟶ l) net ∧ (g ⟶ m) net ⇒ ((λx. f x + g x) ⟶ (l + m)) net

⊢ ∀net a. ((λx. a) ⟶ a) net

⊢ ∀net f l. eventually (λx. f x = l) net ⇒ (f ⟶ l) net

⊢ ∀f l.
    (f ⟶ l) sequentially ⇔
    ∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ dist extreal_mr1 (f n,l) < e

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

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = 1) ⇒ ∏ f s = 1

⊢ ∀f. ∏ f (count 2) = f 0 * f 1 ∧ ∏ f (count 3) = f 0 * f 1 * f 2 ∧
      ∏ f (count 4) = f 0 * f 1 * f 2 * f 3 ∧
      ∏ f (count 5) = f 0 * f 1 * f 2 * f 3 * f 4

⊢ ∀f. ∏ f (count 1) = f 0

⊢ ∀f n. ∏ f (count (SUC n)) = ∏ f (count n) * f n

⊢ ∀f. ∏ f (count 0) = 1

⊢ ∀s s'.
    FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
    ∀f. ∏ f (s ∪ s') = ∏ f s * ∏ f s'

⊢ ∀f. ∏ f ∅ = 1

⊢ ∀s f f'. (∀x. x ∈ s ⇒ f x = f' x) ⇒ ∏ f s = ∏ f' s

⊢ ∀s f'. INJ f' s (IMAGE f' s) ⇒ ∀f. ∏ f (IMAGE f' s) = ∏ (f ∘ f') s

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

⊢ ∀f s. FINITE s ⇒ ∏ (λx. Normal (f x)) s = Normal (∏ f s)

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ⇒ ∏ f s ≠ −∞ ∧ ∏ f s ≠ +∞

⊢ ∀s. FINITE s ⇒ ∏ (λx. 1) s = 1

⊢ ∀f a b. a ≠ b ⇒ ∏ f {a; b} = f a * f b

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

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

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

⊢ ∀s t f.
    FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t DIFF s ⇒ f x = 1) ⇒
    ∏ f t = ∏ f s

⊢ ∀s t f.
    FINITE t ∧ FINITE s ∧ s ⊆ t ⇒
    ∏ (λx. if x ∈ s then f x else 1) t = ∏ f s

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

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

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

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

⊢ ∀s. FINITE s ⇒
      ∀f f'.
        (∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
        (∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ⇒
        ∑ (λx. f x + f' x) s = ∑ f s + ∑ f' s

⊢ ∀f s.
    FINITE s ⇒
    ∑ f s = FOLDR (λe acc. f e + acc) 0 (REVERSE (SET_TO_LIST s))

⊢ ∀s. FINITE s ⇒
      ∀f c.
        ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ∧ c ≠ 0 ⇒
        ∑ (λx. f x / Normal c) s = ∑ f s / Normal c

⊢ ∀s. FINITE s ⇒
      ∀f c.
        (∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
        ∑ (λx. Normal c * f x) s = Normal c * ∑ f s

⊢ ∀f. (∀x. f x ≠ +∞) ∨ (∀x. f x ≠ −∞) ⇒
      ∑ f (count 2) = f 0 + f 1 ∧ ∑ f (count 3) = f 0 + f 1 + f 2 ∧
      ∑ f (count 4) = f 0 + f 1 + f 2 + f 3 ∧
      ∑ f (count 5) = f 0 + f 1 + f 2 + f 3 + f 4

⊢ ∀f. ∑ f (count 1) = f 0

⊢ ∀f n.
    (∀m. m ≤ n ⇒ f m ≠ −∞) ∨ (∀m. m ≤ n ⇒ f m ≠ +∞) ⇒
    ∑ f (count (SUC n)) = ∑ f (count n) + f n

⊢ ∀f. ∑ f (count 0) = 0

⊢ ∀f s1 s2.
    FINITE s1 ∧ FINITE s2 ∧
    ((∀s. s ∈ s1 × s2 ⇒ f s ≠ −∞) ∨ ∀s. s ∈ s1 × s2 ⇒ f s ≠ +∞) ⇒
    ∑ (λ(x,y). f (x,y)) (s1 × s2) = ∑ (λ(y,x). f (x,y)) (s2 × s1)

⊢ ∀s s'.
    FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
    ∀f. (∀x. x ∈ s ∪ s' ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ∪ s' ⇒ f x ≠ +∞) ⇒
        ∑ f (s ∪ s') = ∑ f s + ∑ f s'

⊢ ∀f. ∑ f ∅ = 0

⊢ ∀s. FINITE s ⇒
      ∀f f'.
        ((∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
         ∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ∧ (∀x. x ∈ s ⇒ f x = f' x) ⇒
        ∑ f s = ∑ f' s

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

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

⊢ ∀f s.
    FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃i. i ∈ s ∧ f i = +∞) ⇒ ∑ f s = +∞

⊢ ∀f g N.
    (∀n. n < N ⇒ g n = 0) ∧ (∀n. 0 ≤ f n ∧ f n = g (n + N)) ⇒
    ∀n. ∑ f (count n) = ∑ g (count (n + N))

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

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

⊢ ∀s P f.
    FINITE s ∧ (∀x. x ∈ s ⇒ P x) ∧
    ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
    ∑ (λx. if P x then f x else 0) s = ∑ f s

⊢ ∀s. FINITE s ⇒
      ∀f'.
        INJ f' s (IMAGE f' s) ⇒
        ∀f. (∀x. x ∈ IMAGE f' s ⇒ f x ≠ −∞) ∨
            (∀x. x ∈ IMAGE f' s ⇒ f x ≠ +∞) ⇒
            ∑ f (IMAGE f' s) = ∑ (f ∘ f') s

⊢ ∀f. (∀x. f x ≠ +∞) ∨ (∀x. f x ≠ −∞) ⇒
      ∀e s. FINITE s ⇒ ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

⊢ ∀s. FINITE s ⇒
      ∀f s'.
        ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ∧
        (∀x. x ∉ s' ⇒ f x = 0) ⇒
        ∑ f (s ∩ s') = ∑ f s

⊢ ∀s. FINITE s ⇒
      ∀f. (∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
          ∑ f (s ∩ (λp. f p ≠ 0)) = ∑ f s

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

⊢ ∀s. FINITE s ⇒
      ∀f. (∀x. x ∈ s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
          ∑ f s = ∑ (λx. if x ∈ s then f x else 0) s

⊢ ∀s f z.
    FINITE s ∧ ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
    ∑ f s = ∑ (λx. if x ∈ s then f x else z) s

⊢ ∀f s.
    FINITE s ∧ ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
    ∑ (λx. -f x) s = -∑ f s

⊢ ∀s. FINITE s ⇒
      ∀f f'.
        ((∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ −∞) ∨
         ∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ +∞) ∧ (∀x. x ∈ s ⇒ f x ≤ f' x) ⇒
        ∑ f s ≤ ∑ f' s

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

⊢ ∀f g s.
    FINITE s ∧ s ≠ ∅ ∧
    ((∀x. x ∈ s ⇒ f x ≠ −∞ ∧ g x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞ ∧ g x ≠ +∞) ∧
    (∀x. x ∈ s ⇒ f x < g x) ⇒
    ∑ f s < ∑ g s

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

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

⊢ ∀f s. FINITE s ⇒ ∑ (λx. Normal (f x)) s = Normal (∑ f s)

⊢ ∀f s.
    (FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞) ⇒ ∑ f s ≠ −∞) ∧
    (FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒ ∑ f s ≠ +∞)

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞) ⇒ ∑ f s ≠ −∞

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒ ∑ f s ≠ +∞

⊢ ∀f m n.
    m ≤ n ∧ (∀n. 0 ≤ f n) ⇒
    ∑ f (count n) = ∑ f (count m) + ∑ (λi. f (i + m)) (count (n − m))

⊢ ∀s. FINITE s ⇒
      ∀g. g PERMUTES s ⇒
          ∀f. (∀x. x ∈ IMAGE g s ⇒ f x ≠ −∞) ∨
              (∀x. x ∈ IMAGE g s ⇒ f x ≠ +∞) ⇒
              ∑ (f ∘ g) s = ∑ f s

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

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

⊢ ∀f s.
    FINITE s ⇒
    (∀x. x ∈ s ⇒ f x ≠ −∞) ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
    (∑ f s)² = ∑ (λ(i,j). f i * f j) (s × s)

⊢ ∀f s.
    FINITE s ⇒
    ∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ∨ (∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ⇒
        ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

⊢ ∀f s.
    FINITE s ⇒
    ∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ⇒
        ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

⊢ ∀f s.
    FINITE s ⇒
    ∀e. (∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ⇒
        ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

⊢ ∀s f.
    FINITE s ⇒
    (∀x. x ∈ s ⇒ f x ≠ −∞) ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒
    ∑ (λx. real (f x)) s = real (∑ f s)

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

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

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

⊢ ∀s. FINITE s ⇒
      ∀f f'.
        (∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f' x ≠ +∞) ∨
        (∀x. x ∈ s ⇒ f x ≠ +∞ ∧ f' x ≠ −∞) ⇒
        ∑ (λx. f x − f' x) s = ∑ f s − ∑ f' s

⊢ ∀s s' f.
    FINITE s ∧ FINITE s' ∧
    ((∀x. x ∈ s × s' ⇒ f (FST x) (SND x) ≠ −∞) ∨
     ∀x. x ∈ s × s' ⇒ f (FST x) (SND x) ≠ +∞) ⇒
    ∑ (λx. ∑ (f x) s') s = ∑ (λx. f (FST x) (SND x)) (s × s')

⊢ ∀f a b c d.
    (∀m n. 0 ≤ f m n) ∧ a ≤ c ∧ b ≤ d ⇒
    ∑ (λi. ∑ (f i) (count a)) (count b) ≤
    ∑ (λi. ∑ (f i) (count c)) (count d)

⊢ ∀f. ∑ f ∅ = 0 ∧ (∀e. ∑ f {e} = f e) ∧
      ∀e s.
        FINITE s ∧
        ((∀x. x ∈ e INSERT s ⇒ f x ≠ +∞) ∨ ∀x. x ∈ e INSERT s ⇒ f x ≠ −∞) ⇒
        ∑ f (e INSERT s) = f e + ∑ f (s DELETE e)

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

⊢ ∀s. FINITE s ⇒
      ∀f t.
        ((∀x. x ∈ s ⇒ f x ≠ −∞) ∨ ∀x. x ∈ s ⇒ f x ≠ +∞) ∧
        (∀x. x ∈ t ⇒ f x = 0) ⇒
        ∑ f s = ∑ f (s DIFF t)

⊢ ∀f n. (∀n. 0 ≤ f n) ⇒ ∑ f (count n) ≤ suminf f

⊢ ∀P P' f.
    (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ⇒
    ∃g. (∀n. g n ∈ P') ∧ sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P

⊢ ∀f P P'.
    (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ∧ P = IMAGE f P' ∧
    (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ∧ (∀x. g1 x ≤ g2 x) ⇒ f g1 ≤ f g2) ∧
    (∀g1 g2. g1 ∈ P' ∧ g2 ∈ P' ⇒ (λx. max (g1 x) (g2 x)) ∈ P') ⇒
    ∃g. (∀n. g n ∈ P') ∧ (∀x n. g n x ≤ g (SUC n) x) ∧
        sup (IMAGE (λn. f (g n)) 𝕌(:num)) = sup P

⊢ ∀P. (∃x. P x) ∧ (∃z. z ≠ +∞ ∧ ∀x. P x ⇒ x ≤ z) ⇒
      ∃x. (∀n. x n ∈ P) ∧ (∀n. x n ≤ x (SUC n)) ∧
          sup (IMAGE x 𝕌(:num)) = sup P

⊢ ∀f x. (abs ∘ f) x = f⁺ x + f⁻ x

⊢ ∀f. abs ∘ f = (λx. f⁺ x + f⁻ x)

⊢ ∀f x. f x = f⁺ x − f⁻ x

⊢ ∀f. f = (λx. f⁺ x − f⁻ x)

⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)

⊢ ∀f g x.
    f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞ ⇒
    (λx. f x + g x)⁻ x ≤ f⁻ x + g⁻ x

⊢ ∀f. f⁻ = (λx. -min (f x) 0)

⊢ ∀f. f⁻ = (λx. -min 0 (f x))

⊢ ∀f c.
    (0 ≤ c ⇒ (λx. Normal c * f x)⁻ = (λx. Normal c * f⁻ x)) ∧
    (c ≤ 0 ⇒ (λx. Normal c * f x)⁻ = (λx. -Normal c * f⁺ x))

⊢ ∀f c.
    (0 ≤ c ⇒ (λx. c * f x)⁻ = (λx. c * f⁻ x)) ∧
    (c ≤ 0 ⇒ (λx. c * f x)⁻ = (λx. -c * f⁺ x))

⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁻ = (λx. c x * f⁻ x)

⊢ ∀f x. f⁻ x = +∞ ⇒ f⁺ x = 0

⊢ ∀f x. f⁻ x ≤ abs (f x)

⊢ ∀f g. (λx. f x * g x)⁻ = (λx. f⁺ x * g⁻ x + f⁻ x * g⁺ x)

⊢ ∀f x. f x ≠ −∞ ⇒ f⁻ x ≠ +∞

⊢ ∀g x. 0 ≤ g⁻ x

⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁻ = (λx. 0)

⊢ ∀f x. 0 ≤ f x ⇒ f⁻ x = 0

⊢ ∀f x. f x ≤ 0 ⇒ f⁻ x = -f x

⊢ ∀f. (λx. -f x)⁻ = f⁺

⊢ (λx. 0)⁻ = (λx. 0)

⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f

⊢ ∀f g x. (λx. f x + g x)⁺ x ≤ f⁺ x + g⁺ x

⊢ ∀f. f⁺ = (λx. max (f x) 0)

⊢ ∀f. f⁺ = (λx. max 0 (f x))

⊢ ∀f c.
    (0 ≤ c ⇒ (λx. Normal c * f x)⁺ = (λx. Normal c * f⁺ x)) ∧
    (c ≤ 0 ⇒ (λx. Normal c * f x)⁺ = (λx. -Normal c * f⁻ x))

⊢ ∀f c.
    (0 ≤ c ⇒ (λx. c * f x)⁺ = (λx. c * f⁺ x)) ∧
    (c ≤ 0 ⇒ (λx. c * f x)⁺ = (λx. -c * f⁻ x))

⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁺ = (λx. c x * f⁺ x)

⊢ ∀f x. f⁺ x = +∞ ⇒ f⁻ x = 0

⊢ ∀f x. f⁺ x ≤ abs (f x)

⊢ ∀f g. (λx. f x * g x)⁺ = (λx. f⁺ x * g⁺ x + f⁻ x * g⁻ x)

⊢ ∀g. (∀x. g x ≤ 0) ⇒ g⁺ = (λx. 0)

⊢ ∀f x. f x ≠ +∞ ⇒ f⁺ x ≠ +∞

⊢ ∀g x. 0 ≤ g⁺ x

⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁺ = g

⊢ ∀f x. 0 ≤ f x ⇒ f⁺ x = f x

⊢ ∀f x. f x ≤ 0 ⇒ f⁺ x = 0

⊢ ∀f. (λx. -f x)⁺ = f⁻

⊢ (λx. 0)⁺ = (λx. 0)

⊢ ∀s. abs ∘ 𝟙 s = 𝟙 s

⊢ ∀f s. abs ∘ (λx. f x * 𝟙 s x) = (λx. (abs ∘ f) x * 𝟙 s x)

⊢ ∀s t x y. 𝟙 (s × t) (x,y) = 𝟙 s x * 𝟙 t y

⊢ ∀A B. 𝟙 (A DIFF B) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)

⊢ ∀A B sp.
    A ⊆ sp ∧ B ⊆ sp ⇒ 𝟙 (A ∩ (sp DIFF B)) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)

⊢ ∀x. 𝟙 ∅ x = 0

⊢ ∀A B. 𝟙 (A ∩ B) = (λt. 𝟙 A t * 𝟙 B t)

⊢ ∀A B. 𝟙 (A ∩ B) = (λt. min (𝟙 A t) (𝟙 B t))

⊢ ∀s x. 𝟙 s x ≤ 1

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

⊢ ∀A B. (λt. 𝟙 A t * 𝟙 B t) = (λt. 𝟙 (A ∩ B) t)

⊢ ∀s x. 𝟙 s x ≠ −∞ ∧ 𝟙 s x ≠ +∞

⊢ ∀s x. 0 ≤ 𝟙 s x

⊢ ∀x y. x ≠ y ⇒ 𝟙 {x} y = 0

⊢ ∀x y. x = y ⇒ 𝟙 {x} y = 1

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. 𝟙 A t + 𝟙 B t − 𝟙 (A ∩ B) t)

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. max (𝟙 A t) (𝟙 B t))

⊢ ∀A B. 𝟙 (A ∪ B) = (λt. min (𝟙 A t + 𝟙 B t) 1)

⊢ ∀x. 𝟙 𝕌(:α) x = 1

⊢ ∀top f.
    f ∈ C_b top ⇔
    continuous_map (top,euclidean) f ∧ bounded (IMAGE f 𝕌(:α))

⊢ ∀f z.
    z ∈ flat_values f ⇔
    ∃a b.
      a < b ∧ (∀x. a < x ∧ x < b ⇒ f x = z) ∧ (∀x. x < a ⇒ f x < z) ∧
      ∀x. b < x ⇒ z < f x

⊢ ∀a b x. x ∈ open_interval a b ⇔ a < x ∧ x < b

⊢ ∀f l.
    ((λn. f n) ⟶ l) sequentially ⇒
    ((λn. ∑ f (count (SUC n)) / &SUC n) ⟶ l) sequentially

⊢ ∀a l.
    (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ⇒
    ((real ∘ a ⟶ l) sequentially ⇔
     ∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ abs (a n − Normal l) < Normal e)

⊢ Lipschitz_continuous_map (mr1,extreal_mr1) Normal

⊢ ∀f s s'.
    FINITE s ∧ FINITE s' ∧ (∀x y. x ∈ s ∧ y ∈ s' ⇒ f x y ≠ −∞) ⇒
    ∑ (λx. ∑ (f x) s') s = ∑ (λx. ∑ (λy. f y x) s) s'

⊢ countable ℚ꙳

⊢ ∀x y. x < y ⇒ ∃r. r ∈ ℚ꙳ ∧ x < r ∧ r < y

⊢ ∀x. x ∈ ℚ꙳ ⇒ ∃y. x = Normal y

⊢ ∀x. x ≠ +∞ ⇒ ∃n. x ≤ &n

⊢ ∀x. x ≠ −∞ ⇒ ∃n. -&n ≤ x

⊢ abs 0 = 0

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

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

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

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ 0 ⇒ abs (x / y) = abs x / abs y

⊢ ∀x y. y ≠ 0 ⇒ abs (x / Normal y) = abs x / Normal (abs y)

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

⊢ ∀x. 0 < abs x ⇔ x ≠ 0

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

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

⊢ ∀x. abs x ≤ x² + 1

⊢ ∀x. abs x = max x (-x)

⊢ ∀x y. abs (x * y) = abs x * abs y

⊢ ∀x. x < 0 ⇒ abs x = -x

⊢ ∀x. x ≤ 0 ⇒ abs x = -x

⊢ ∀x. abs (-x) = abs x

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞

⊢ ∀x. abs x ≠ 0 ⇔ x ≠ 0

⊢ ∀x. 0 ≤ abs x

⊢ ∀x. (abs x)² = x²

⊢ ∀x n m. n ≤ m ⇒ abs x pow n ≤ 1 + abs x pow m

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs (real x) = real (abs x)

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

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) = abs (y − x)

⊢ ∀x y. abs (x − y) = abs (y − x)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y

⊢ ∀x y. abs (x + y) ≤ abs x + abs y

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) ≤ abs x + abs y

⊢ ∀x y. abs (x − y) ≤ abs x + abs y

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (x − y)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (y − x)

⊢ ∀x y. abs x ≤ abs y + abs (x − y)

⊢ ∀x y. abs x ≤ abs y + abs (y − x)

⊢ ∀x k. 0 ≤ k ⇒ (k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x)

⊢ ∀a b c d.
    a ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ d ≠ +∞ ⇒ a − b + (c − d) = a + c − (b + d)

⊢ ∀x y z.
    x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ +∞ ⇒
    x + (y + z) = x + y + z

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y = y + x

⊢ ∀x y. Normal x + y = y + Normal x

⊢ (∀x. x ≠ −∞ ⇒ x + +∞ = +∞ ∧ +∞ + x = +∞) ∧
  ∀x. x ≠ +∞ ⇒ x + −∞ = −∞ ∧ −∞ + x = −∞

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z

⊢ ∀x y z. y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z

⊢ ∀r y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    Normal r * (y + z) = Normal r * y + Normal r * z

⊢ ∀r y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    Normal r * (y + z) = Normal r * y + Normal r * z

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ⇒ x * (y + z) = x * y + x * z

⊢ ∀x. 0 + x = x

⊢ ∀x y. (x ≠ −∞ ∧ y ≠ −∞ ⇒ x + y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y ≠ +∞)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (x + y)² = x² + y² + 2 * x * y

⊢ ∀x y. 0 < x ∧ x ≠ +∞ ∧ 0 ≤ y ⇒ (x + y)² = x² + y² + 2 * x * y

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ (y + z) * x = y * x + z * x

⊢ ∀x y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    (y + z) * Normal x = y * Normal x + z * Normal x

⊢ ∀x y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    (y + z) * Normal x = y * Normal x + z * Normal x

⊢ ∀x. x + 0 = x

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x + y − y = x

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ y + x − y = x

⊢ ∀x r. x + Normal r − Normal r = x

⊢ ∀x k. abs x ≤ Normal k ⇒ x ≠ −∞ ∧ x ≠ +∞

⊢ ∀p q.
    0 < p ∧ 0 < q ∧ p⁻¹ + q⁻¹ = 1 ⇒
    1 ≤ p ∧ 1 ≤ q ∧ (p = 1 ⇔ q = +∞) ∧ (q = 1 ⇔ p = +∞)

⊢ continuous_map (euclidean,ext_euclidean) Normal

⊢ continuous_map (ext_euclidean,euclidean) real

⊢ ∀s. s = {interval (c,d) | c < d} ∧ disjoint s ⇒ countable s

⊢ ∀s. s ⊆ {open_interval c d | c < d} ∧ disjoint s ⇒ countable s

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ countable {(a,b) | (a,b) flat_area_of f}

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ countable {x | x jumping_point_of f}

⊢ ∀x1 y1 x2 y2.
    dist extreal_mr1 (x1 + y1,x2 + y2) ≤
    dist extreal_mr1 (x1,x2) + dist extreal_mr1 (y1,y2)

⊢ ∀x y z.
    x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒ x / z + y / z = (x + y) / z

⊢ ∀x y z.
    (x ≠ +∞ ∧ y ≠ +∞ ∨ x ≠ −∞ ∧ y ≠ −∞) ∧ z ≠ 0 ∧ z ≠ +∞ ∧ z ≠ −∞ ⇒
    x / z + y / z = (x + y) / z

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = y⁻¹ * x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = x * y⁻¹

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ x / +∞ = 0 ∧ x / −∞ = 0

⊢ ∀x r. r ≠ 0 ⇒ x = x / Normal r * Normal r

⊢ ∀x y. y ≠ 0 ⇒ Normal x / y ≠ +∞ ∧ Normal x / y ≠ −∞

⊢ ∀x. x / 1 = x

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x / x = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x / x = 1

⊢ ∀x y z.
    x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒ x / z − y / z = (x − y) / z

⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0

⊢ ∀a b c d.
    b ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ c ≠ +∞ ⇒ (a + b = c + d ⇔ a − c = d − b)

⊢ ∀x y. -x = -y ⇔ x = y

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x = y − z ⇔ x + z = y)

⊢ ∀x y z. x = y − Normal z ⇔ x + Normal z = y

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y = z ⇔ x = z + y)

⊢ ∀x y z. x = Normal z − y ⇔ y = Normal z − x

⊢ ∀x y z. x = y ∧ y ≤ z ⇒ x ≤ z

⊢ exp 0 = 1

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ exp (x + y) = exp x * exp y

⊢ ∀x. 1 + x ≤ exp x

⊢ ∀x. 1 − x ≤ exp (-x)

⊢ ∀x y. exp x ≤ exp y ⇔ x ≤ y

⊢ ∀x. x ≠ −∞ ⇒ exp (-x) = (exp x)⁻¹

⊢ ∀x. 0 ≤ exp x

⊢ ∀x. x ≠ −∞ ⇒ 0 < exp x

⊢ ∀s. ext_bounded s ⇔ ∃k. 0 ≤ k ∧ ∀x. x ∈ s ⇒ abs x ≤ Normal k

⊢ ∀a b.
    ext_bounded (IMAGE a 𝕌(:num)) ∧ ext_bounded (IMAGE b 𝕌(:num)) ⇒
    liminf a + liminf b ≤ liminf (λn. a n + b n)

⊢ ∀a. liminf a = -limsup (numeric_negate ∘ a)

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ abs (liminf a) ≤ k

⊢ ∀f c. 0 ≤ c ⇒ liminf (λn. Normal c * f n) = Normal c * liminf f

⊢ ∀c. liminf (λn. c) = c

⊢ ∀a. (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ liminf a ≠ +∞ ∧ liminf a ≠ −∞ ⇒
      ∃f. (∀m n. m < n ⇒ f m < f n) ∧
          (real ∘ a ∘ f ⟶ real (liminf a)) sequentially

⊢ ∀a. liminf a ≤ limsup a

⊢ ∀a f l.
    (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ (∀m n. m < n ⇒ f m < f n) ∧
    (real ∘ a ∘ f ⟶ l) sequentially ⇒
    liminf a ≤ Normal l

⊢ ∀a c. (∀n. c ≤ a n) ⇒ c ≤ liminf a

⊢ ∀p q. (∀n. p n ≤ q n) ⇒ liminf p ≤ liminf q

⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ liminf a

⊢ ∀a c. (∀n. a n ≤ c) ⇒ liminf a ≤ c

⊢ ∀a b.
    ext_bounded (IMAGE a 𝕌(:num)) ∧ ext_bounded (IMAGE b 𝕌(:num)) ⇒
    limsup (λn. a n + b n) ≤ limsup a + limsup b

⊢ ∀a. limsup a = -liminf (numeric_negate ∘ a)

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ abs (limsup a) ≤ k

⊢ ∀f c. 0 ≤ c ⇒ limsup (λn. Normal c * f n) = Normal c * limsup f

⊢ ∀c. limsup (λn. c) = c

⊢ ∀a. (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ limsup a ≠ +∞ ∧ limsup a ≠ −∞ ⇒
      ∃f. (∀m n. m < n ⇒ f m < f n) ∧
          (real ∘ a ∘ f ⟶ real (limsup a)) sequentially

⊢ ∀a f l.
    (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ∧ (∀m n. m < n ⇒ f m < f n) ∧
    (real ∘ a ∘ f ⟶ l) sequentially ⇒
    Normal l ≤ limsup a

⊢ ∀a c. (∀n. c ≤ a n) ⇒ c ≤ limsup a

⊢ ∀p q. (∀n. p n ≤ q n) ⇒ limsup p ≤ limsup q

⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ limsup a

⊢ ∀f. sup (IMAGE (λm. limsup (λn. f n m)) 𝕌(:num)) ≤
      limsup (λn. sup (IMAGE (f n) 𝕌(:num)))

⊢ ∀a l.
    (∀n. a n ≠ +∞ ∧ a n ≠ −∞) ⇒
    ((real ∘ a ⟶ l) sequentially ⇔
     limsup a = Normal l ∧ liminf a = Normal l)

⊢ ∀f l.
    (∀n. f n ≠ +∞ ∧ f n ≠ −∞) ∧ l ≠ +∞ ∧ l ≠ −∞ ⇒
    ((f ⟶ l) sequentially ⇔ limsup f = l ∧ liminf f = l)

⊢ ∀f J.
    FINITE J ∧ (∀i. ext_bounded (IMAGE (λn. f n i) 𝕌(:num))) ⇒
    limsup (λn. ∑ (f n) J) ≤ ∑ (λi. limsup (λn. f n i)) J

⊢ ∀a c. (∀n. a n ≤ c) ⇒ limsup a ≤ c

⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n

⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)

⊢ suminf (λn. 0) = 0

⊢ ∀f g h.
    (∀m n. 0 ≤ f m n) ∧ (∀n. suminf (f n) = g n) ∧ suminf g < +∞ ∧
    BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    suminf (UNCURRY f ∘ h) = suminf g

⊢ ∀f g h.
    (∀m n. 0 ≤ f m n) ∧ (∀n. suminf (f n) = g n) ∧
    BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    suminf (UNCURRY f ∘ h) = suminf g

⊢ ∀f g.
    (∀n. 0 ≤ f n ∧ 0 ≤ g n) ⇒ suminf (λn. f n + g n) = suminf f + suminf g

⊢ ∀f g h.
    (∀n. 0 ≤ f n) ∧ (∀n. 0 ≤ g n) ∧ (∀n. h n = f n + g n) ⇒
    suminf h = suminf f + suminf g

⊢ ∀f. (∀n. 0 ≤ f n) ⇒
      suminf (λx. f x) = sup {∑ (λi. f i) (count n) | n ∈ 𝕌(:num)}

⊢ ∀f. (∀n. 0 ≤ f n) ⇒ suminf (λx. f x) = sup {∑ f (count n) | n | T}

⊢ ∀f c. 0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒ suminf (λn. c * f n) = c * suminf f

⊢ ∀f c.
    0 ≤ c ∧ (∀n. 0 ≤ f n) ∧ (∀n. f n < +∞) ⇒
    suminf (λn. Normal c * f n) = Normal c * suminf f

⊢ ∀f g. (∀n. f n = g n) ⇒ suminf f = suminf g

⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)) ⇒ suminf f = +∞

⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f = +∞ ⇒ ∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)

⊢ ∀f g N.
    (∀n. n < N ⇒ g n = 0) ∧ (∀n. 0 ≤ f n ∧ f n = g (n + N)) ⇒
    suminf f = suminf g

⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f < +∞ ⇒ ∀n. f n < +∞

⊢ ∀f g. (∀n. 0 ≤ g n) ∧ (∀n. g n ≤ f n) ⇒ suminf g ≤ suminf f

⊢ ∀f. (∀m n. 0 ≤ f m n) ⇒
      suminf (λn. suminf (λm. f m n)) = suminf (λm. suminf (λn. f m n))

⊢ ∀f m. (∀n. 0 ≤ f n) ⇒ suminf f = ∑ f (count m) + suminf (λi. f (i + m))

⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃n. f n = +∞) ⇒ suminf f = +∞

⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒ suminf (real ∘ g) = real (suminf g)

⊢ ∀f n.
    (∀i x. i < n ⇒ 0 ≤ f i x) ⇒
    ∑ (suminf ∘ f) (count n) = suminf (λx. ∑ (λi. f i x) (count n))

⊢ ∀f n.
    (∀i x. i < n ⇒ 0 ≤ f i x) ⇒
    ∑ (λx. suminf (f x)) (count n) = suminf (λx. ∑ (λi. f i x) (count n))

⊢ ∀r. 0 ≤ r ⇒ suminf (λn. if n = 0 then r else 0) = r

⊢ ∀m r. 0 ≤ r ⇒ suminf (λn. if n = m then r else 0) = r

⊢ ∀f g.
    (∀n. 0 ≤ g n ∧ g n ≤ f n) ∧ suminf f ≠ +∞ ⇒
    suminf (λi. f i − g i) = suminf f − suminf g

⊢ ∀f n. (∀n. 0 ≤ f n) ∧ (∀m. n ≤ m ⇒ f m = 0) ⇒ suminf f = ∑ f (count n)

⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (λn. Normal (r n)) ≠ +∞ ⇒
      suminf (λn. Normal (r n)) = Normal (suminf r)

⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (Normal ∘ r) < +∞ ⇒
      suminf (Normal ∘ r) = Normal (suminf r)

⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒ summable (real ∘ g)

⊢ ∀f. (∀i m n. m ≤ n ⇒ f m i ≤ f n i) ∧ (∀n i. 0 ≤ f n i) ⇒
      suminf (λi. sup {f n i | n ∈ 𝕌(:num)}) =
      sup {suminf (λi. f n i) | n ∈ 𝕌(:num)}

⊢ ∀f. (∀n. f n = 0) ⇒ suminf f = 0

⊢ ∀f l net.
    (f ⟶ l) net ⇔
    ∀e. 0 < e ⇒ eventually (λx. dist extreal_mr1 (f x,l) < e) net

⊢ (0 ≤ +∞ ⇔ T) ∧ (0 < +∞ ⇔ T) ∧ (+∞ ≤ 0 ⇔ F) ∧ (+∞ < 0 ⇔ F) ∧
  (0 = +∞ ⇔ F) ∧ (+∞ = 0 ⇔ F) ∧ (0 ≤ −∞ ⇔ F) ∧ (0 < −∞ ⇔ F) ∧
  (−∞ ≤ 0 ⇔ T) ∧ (−∞ < 0 ⇔ T) ∧ (0 = −∞ ⇔ F) ∧ (−∞ = 0 ⇔ F) ∧
  (∀r. 0 ≤ Normal r ⇔ 0 ≤ r) ∧ (∀r. 0 < Normal r ⇔ 0 < r) ∧
  (∀r. 0 = Normal r ⇔ r = 0) ∧ (∀r. Normal r ≤ 0 ⇔ r ≤ 0) ∧
  (∀r. Normal r < 0 ⇔ r < 0) ∧ ∀r. Normal r = 0 ⇔ r = 0

⊢ ∀a a'. Normal a = Normal a' ⇔ a = a'

⊢ (1 ≤ +∞ ⇔ T) ∧ (1 < +∞ ⇔ T) ∧ (+∞ ≤ 1 ⇔ F) ∧ (+∞ < 1 ⇔ F) ∧
  (1 = +∞ ⇔ F) ∧ (+∞ = 1 ⇔ F) ∧ (1 ≤ −∞ ⇔ F) ∧ (1 < −∞ ⇔ F) ∧
  (−∞ ≤ 1 ⇔ T) ∧ (−∞ < 1 ⇔ T) ∧ (1 = −∞ ⇔ F) ∧ (−∞ = 1 ⇔ F) ∧
  (∀r. 1 ≤ Normal r ⇔ 1 ≤ r) ∧ (∀r. 1 < Normal r ⇔ 1 < r) ∧
  (∀r. 1 = Normal r ⇔ r = 1) ∧ (∀r. Normal r ≤ 1 ⇔ r ≤ 1) ∧
  (∀r. Normal r < 1 ⇔ r < 1) ∧ ∀r. Normal r = 1 ⇔ r = 1

⊢ abs (Normal x) = Normal (abs x) ∧ abs −∞ = +∞ ∧ abs +∞ = +∞

⊢ Normal x + Normal y = Normal (x + y) ∧ Normal v0 + −∞ = −∞ ∧
  Normal v0 + +∞ = +∞ ∧ −∞ + Normal v1 = −∞ ∧ +∞ + Normal v1 = +∞ ∧
  −∞ + −∞ = −∞ ∧ +∞ + +∞ = +∞

⊢ ∀x y. Normal x + Normal y = Normal (x + y)

⊢ -−∞ = +∞ ∧ -+∞ = −∞ ∧ ∀x. -Normal x = Normal (-x)

⊢ ∀x. x = −∞ ∨ x = +∞ ∨ ∃r. x = Normal r

⊢ extreal_dist (Normal x) (Normal y) = dist (bounded_metric mr1) (x,y) ∧
  extreal_dist +∞ +∞ = 0 ∧ extreal_dist −∞ −∞ = 0 ∧
  extreal_dist −∞ +∞ = 1 ∧ extreal_dist −∞ (Normal v5) = 1 ∧
  extreal_dist +∞ −∞ = 1 ∧ extreal_dist +∞ (Normal v7) = 1 ∧
  extreal_dist (Normal v3) −∞ = 1 ∧ extreal_dist (Normal v3) +∞ = 1

⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ P +∞ +∞ ∧ P −∞ −∞ ∧ P −∞ +∞ ∧
      (∀v5. P −∞ (Normal v5)) ∧ P +∞ −∞ ∧ (∀v7. P +∞ (Normal v7)) ∧
      (∀v3. P (Normal v3) −∞) ∧ (∀v3. P (Normal v3) +∞) ⇒
      ∀v v1. P v v1

⊢ ismet (UNCURRY extreal_dist)

⊢ ∀x y.
    extreal_dist (Normal x) (Normal y) = abs (x − y) / (1 + abs (x − y))

⊢ ∀x y. extreal_dist (Normal x) (Normal y) = 1 − (1 + abs (x − y))⁻¹

⊢ −∞ ≠ +∞ ∧ (∀a. −∞ ≠ Normal a) ∧ ∀a. +∞ ≠ Normal a

⊢ (∀r. Normal r / +∞ = Normal 0) ∧ (∀r. Normal r / −∞ = Normal 0) ∧
  ∀x r. r ≠ 0 ⇒ x / Normal r = x * (Normal r)⁻¹

⊢ ∀x y. y ≠ 0 ⇒ Normal x / Normal y = Normal (x / y)

⊢ ∀x. x + x = 2 * x

⊢ ∀x. Normal x = 0 ⇔ x = 0

⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
  ∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹

⊢ ∀x. x ≠ 0 ⇒ (Normal x)⁻¹ = Normal x⁻¹

⊢ (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (−∞ ≤ v0 ⇔ T) ∧ (+∞ ≤ +∞ ⇔ T) ∧
  (Normal v5 ≤ +∞ ⇔ T) ∧ (+∞ ≤ −∞ ⇔ F) ∧ (Normal v6 ≤ −∞ ⇔ F) ∧
  (+∞ ≤ Normal v8 ⇔ F)

⊢ ∀x y. Normal x ≤ Normal y ⇔ x ≤ y

⊢ (∀x y. Normal x ≤ Normal y ⇔ x ≤ y) ∧ (∀x. −∞ ≤ x ⇔ T) ∧
  (∀x. x ≤ +∞ ⇔ T) ∧ (∀x. Normal x ≤ −∞ ⇔ F) ∧ (∀x. +∞ ≤ Normal x ⇔ F) ∧
  (+∞ ≤ −∞ ⇔ F)

⊢ ∀f l.
    (∃N. ∀n. N ≤ n ⇒ f n ≠ +∞ ∧ f n ≠ −∞) ∧ l ≠ +∞ ∧ l ≠ −∞ ⇒
    ((f ⟶ l) sequentially ⇔ (real ∘ f ⟶ real l) sequentially)

⊢ ∀f r.
    (∃N. ∀n. N ≤ n ⇒ f n ≠ +∞ ∧ f n ≠ −∞) ⇒
    ((f ⟶ Normal r) sequentially ⇔ (real ∘ f ⟶ r) sequentially)

⊢ ∀x y. x < y ⇔ ¬(y ≤ x)

⊢ ∀x y. Normal x < Normal y ⇔ x < y

⊢ (∀x y. Normal x < Normal y ⇔ x < y) ∧ (∀x. x < −∞ ⇔ F) ∧
  (∀x. +∞ < x ⇔ F) ∧ (∀x. Normal x < +∞ ⇔ T) ∧ (∀x. −∞ < Normal x ⇔ T) ∧
  (−∞ < +∞ ⇔ T)

⊢ ∀x y. max x y = if x ≤ y then y else x

⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y

⊢ ∀x y. min x y = if x ≤ y then x else y

⊢ dist extreal_mr1 (Normal r,+∞) = 1 ∧ dist extreal_mr1 (Normal r,−∞) = 1 ∧
  dist extreal_mr1 (+∞,Normal r) = 1 ∧ dist extreal_mr1 (−∞,Normal r) = 1 ∧
  dist extreal_mr1 (+∞,−∞) = 1 ∧ dist extreal_mr1 (−∞,+∞) = 1

⊢ ∀x y. dist extreal_mr1 (x,y) ≤ 1

⊢ ∀x y. dist extreal_mr1 (Normal x,Normal y) < 1

⊢ ∀x y.
    dist extreal_mr1 (Normal x,Normal y) = abs (x − y) / (1 + abs (x − y))

⊢ ∀x y. dist extreal_mr1 (Normal x,Normal y) = 1 − (1 + abs (x − y))⁻¹

⊢ dist extreal_mr1 = UNCURRY extreal_dist

⊢ −∞ * −∞ = +∞ ∧ −∞ * +∞ = −∞ ∧ +∞ * −∞ = −∞ ∧ +∞ * +∞ = +∞ ∧
  Normal x * −∞ = (if x = 0 then Normal 0 else if 0 < x then −∞ else +∞) ∧
  −∞ * Normal y = (if y = 0 then Normal 0 else if 0 < y then −∞ else +∞) ∧
  Normal x * +∞ = (if x = 0 then Normal 0 else if 0 < x then +∞ else −∞) ∧
  +∞ * Normal y = (if y = 0 then Normal 0 else if 0 < y then +∞ else −∞) ∧
  Normal x * Normal y = Normal (x * y)

⊢ ∀x y. Normal x * Normal y = Normal (x * y)

⊢ ∀x. Normal x ≠ −∞ ∧ Normal x ≠ +∞

⊢ ∀x y. ¬(x < y) ⇔ y ≤ x

⊢ ∀n. &n = Normal (&n)

⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n

⊢ (∀x. x pow 0 = 1) ∧ ∀n x. x pow SUC n = x pow n * x

⊢ (∀a n. Normal a pow n = Normal (a pow n)) ∧
  (∀n. +∞ pow n = if n = 0 then Normal 1 else +∞) ∧
  ∀n. −∞ pow n = if n = 0 then Normal 1 else if EVEN n then +∞ else −∞

⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ sqrt +∞ = +∞

⊢ ∀x y. x − y = x + -y

⊢ ∀x y. x ≠ −∞ ∧ y ≠ +∞ ∨ x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y = x + -y

⊢ Normal x − Normal y = Normal (x − y) ∧ +∞ − Normal x = +∞ ∧
  −∞ − Normal x = −∞ ∧ Normal x − −∞ = +∞ ∧ Normal x − +∞ = −∞ ∧
  −∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞

⊢ ∀x y. Normal x − Normal y = Normal (x − y)

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ countable (flat_areas f)

⊢ ∀f. flat_values f = IMAGE (inf ∘ IMAGE f) (flat_areas f)

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ countable (flat_values f)

⊢ ∀f x. f⁻ x = -min 0 (f x)

⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)

⊢ ∀f c x.
    (0 ≤ c ⇒ (λx. c * f x)⁻ x = c * f⁻ x) ∧
    (c ≤ 0 ⇒ (λx. c * f x)⁻ x = -c * f⁺ x)

⊢ ∀f c x. 0 ≤ c x ⇒ (λx. c x * f x)⁻ x = c x * f⁻ x

⊢ ∀f s. (λx. f x * 𝟙 s x)⁻ = (λx. f⁻ x * 𝟙 s x)

⊢ ∀f x. f⁺ x = max 0 (f x)

⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f

⊢ ∀f. f⁺ = (λx. if 0 ≤ f x then f x else 0)

⊢ ∀f c x.
    (0 ≤ c ⇒ (λx. c * f x)⁺ x = c * f⁺ x) ∧
    (c ≤ 0 ⇒ (λx. c * f x)⁺ x = -c * f⁻ x)

⊢ ∀f c x. 0 ≤ c x ⇒ (λx. c x * f x)⁺ x = c x * f⁺ x

⊢ ∀f s. (λx. f x * 𝟙 s x)⁺ = (λx. f⁺ x * 𝟙 s x)

⊢ 4 * (1 / 4) = 1

⊢ ((0 < 1 / 4 ∧ 1 / 4 < 1) ∧ 0 < 3 / 4 ∧ 3 / 4 < 1) ∧
  (0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1) ∧ 0 ≤ 3 / 4 ∧ 3 / 4 ≤ 1

⊢ ∀a n. 0 ≤ a ⇒ a pow n = a powr &n

⊢ ∀x. 0 < x ∧ x < 1 ⇒ suminf (λn. x pow n) = (1 − x)⁻¹

⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1

⊢ 2 * (1 / 2) = 1

⊢ ∀x. x / 2 + x / 2 = x

⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞

⊢ suminf (λn. (&SUC n)² ⁻¹) < +∞

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

⊢ ∀s x. ∃r. 𝟙 s x = Normal r ∧ 0 ≤ r ∧ r ≤ 1

⊢ ∀r s b.
    FINITE r ∧ BIGUNION (IMAGE b r) = s ∧
    (∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ⇒
    ∀a. a ⊆ s ⇒ 𝟙 a = (λx. ∑ (λi. 𝟙 (a ∩ b i) x) r)

⊢ ∀a x.
    (∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
    suminf (λi. 𝟙 (a i) x) = 𝟙 (BIGUNION (IMAGE a 𝕌(:num))) x

⊢ (∀x y. x < y ⇒ ¬(y < x)) ∧ (∀x y. x < y ⇒ x ≠ y) ∧
  (∀x y. x < y ⇒ ¬(y ≤ x)) ∧ (∀x y. x < y ⇒ x ≤ y) ∧ ∀x y. x ≤ y ⇒ ¬(y < x)

⊢ ∀f g.
    ext_bounded (IMAGE f 𝕌(:num)) ∧ mono_decreasing f ∧
    ext_bounded (IMAGE g 𝕌(:num)) ∧ mono_decreasing g ⇒
    inf (IMAGE (λn. f n + g n) 𝕌(:num)) =
    inf (IMAGE f 𝕌(:num)) + inf (IMAGE g 𝕌(:num))

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ ∀m. abs (inf {a n | m ≤ n}) ≤ k

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ ∀m. abs (inf (IMAGE a 𝕌(:α))) ≤ k

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

⊢ ∀f c.
    Normal c − inf (IMAGE f 𝕌(:α)) = sup (IMAGE (λn. Normal c − f n) 𝕌(:α))

⊢ ∀P r.
    0 < r ⇒
    inf {x * Normal r | 0 < x ∧ P x} = Normal r * inf {x | 0 < x ∧ P x}

⊢ ∀f c.
    0 ≤ c ⇒
    inf (IMAGE (λn. Normal c * f n) 𝕌(:α)) = Normal c * inf (IMAGE f 𝕌(:α))

⊢ ∀f c J.
    0 ≤ c ∧ J ≠ ∅ ⇒
    inf (IMAGE (λn. Normal c * f n) J) = Normal c * inf (IMAGE f J)

⊢ ∀x. inf (λy. y = x) = x

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

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

⊢ ∀s k. s ≠ ∅ ⇒ inf (IMAGE (λx. k) s) = k

⊢ ∀A. A ≠ ∅ ⇒ ∃f. IMAGE f 𝕌(:num) ⊆ A ∧ inf A = inf {f n | n ∈ 𝕌(:num)}

⊢ inf ∅ = +∞

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

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

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

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

⊢ ∀p x. p x ⇒ inf p ≤ x

⊢ ∀p x. x ∈ p ⇒ inf p ≤ x

⊢ ∀P y. (∃x. P x ∧ x < y) ⇔ inf P < y

⊢ ∀P y. (∃x. x ∈ P ∧ x < y) ⇔ inf P < y

⊢ ∀p. −∞ < inf p ⇒ ∀x. p x ⇒ −∞ < x

⊢ ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ inf p = z

⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ inf p ∈ p

⊢ ∀p q. (∀n. p n ≤ q n) ⇒ inf (IMAGE p 𝕌(:num)) ≤ inf (IMAGE q 𝕌(:num))

⊢ ∀p q. p ⊆ q ⇒ inf q ≤ inf p

⊢ ∀s k. abs (inf s) ≤ Normal k ⇒ Normal (inf (s ∘ Normal)) = inf s

⊢ inf (λx. ∃n. x = -&n) = −∞

⊢ ∀a b. a < b ⇒ inf (open_interval a b) = a

⊢ ∀a m. (∀n. 0 ≤ a n) ⇒ 0 ≤ inf {a n | m ≤ n}

⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ inf (IMAGE a 𝕌(:α))

⊢ ∀f l.
    mono_decreasing f ⇒
    (f ⟶ l ⇔ inf (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)

⊢ ∀f l.
    mono_decreasing f ⇒
    ((f ⟶ l) sequentially ⇔
     inf (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)

⊢ ∀A g.
    A ≠ ∅ ⇒
    ∃f. IMAGE f 𝕌(:num) ⊆ IMAGE g A ∧
        inf {g n | n ∈ A} = inf {f n | n ∈ 𝕌(:num)}

⊢ ∀a. inf {a} = a

⊢ ∀f. (∀m n. m ≤ n ⇒ f n ≤ f m) ⇒
      inf (IMAGE (λn. f (SUC n)) 𝕌(:num)) = inf (IMAGE f 𝕌(:num))

⊢ inf 𝕌(:extreal) = −∞

⊢ ∀r. 0 < r ⇒ +∞ / Normal r = +∞ ∧ −∞ / Normal r = −∞

⊢ +∞ ² = +∞ ∧ −∞ ² = +∞

⊢ ∀a. 0 < a ⇒ +∞ powr a = +∞

⊢ ∀x. x ≠ 0 ⇒ x⁻¹ = 1 / x

⊢ +∞ ⁻¹ = 0 ∧ −∞ ⁻¹ = 0

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ ⁻¹ = x

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)

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

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)

⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x * y)⁻¹ = x⁻¹ * y⁻¹

⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ≠ +∞ ∧ x⁻¹ ≠ −∞

⊢ 1⁻¹ = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < 1 / x

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < x⁻¹

⊢ ∀x. x ≠ 0 ⇒ (0 < x⁻¹ ⇔ x ≠ +∞ ∧ 0 ≤ x)

⊢ ∀x p. 0 < x ∧ 0 < p ∧ p ≠ +∞ ⇒ x⁻¹ powr p = (x powr p)⁻¹

⊢ ∀f. (∀x y. x ≤ y ⇒ f x ≤ f y) ⇒ countable (jumping_area f)

⊢ ∀f x0.
    (∀x y. x ≤ y ⇒ f x ≤ f y) ∧ x0 jumping_point_of f ⇒
    sup {f x | x < Normal x0} < inf {f x | Normal x0 < x}

⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x / z = y ⇔ x = y * z)

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ∧ x ≤ y ⇒ x / z ≤ y / z

⊢ 0 ≤ 1

⊢ 0 ≤ 2

⊢ ∀x. x ≤ abs x ∧ -x ≤ abs x

⊢ ∀k x. k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x

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

⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z

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

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y ≤ x + y ⇔ 0 ≤ x)

⊢ ∀x y. 0 ≤ x ⇒ y ≤ x + y

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ x + y ⇔ 0 ≤ y)

⊢ ∀x y. 0 ≤ y ⇒ x ≤ x + y

⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y

⊢ ∀y z. 0 ≤ y ∧ 0 < z ⇒ 0 ≤ y / Normal z

⊢ ∀x y. (∀e. 0 < e ∧ e ≠ +∞ ⇒ x ≤ y + e) ⇒ x ≤ y

⊢ ∀p x. x ≤ inf p ⇔ ∀y. p y ⇒ x ≤ y

⊢ ∀p x. x ≤ inf p ⇔ ∀y. y ∈ p ⇒ x ≤ y

⊢ ∀P e.
    0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. x ∈ P ∧ x ≤ inf P + e

⊢ (∀x. −∞ ≤ x ∧ x ≤ +∞) ∧ (∀x. x ≤ −∞ ⇔ x = −∞) ∧ ∀x. +∞ ≤ x ⇔ x = +∞

⊢ ∀x. 0 < x ⇒ 0 ≤ x⁻¹

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y ≤ x + z ⇔ y ≤ z)

⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z

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

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y ≤ x * z ⇔ y ≤ z)

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

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ (-x ≤ y ⇔ 0 ≤ x + y)

⊢ ∀x y z. y ≤ z ⇒ x − z ≤ x − y

⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y

⊢ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y

⊢ ∀x y. x ≤ max x y

⊢ ∀x y. y ≤ max x y

⊢ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y

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

⊢ ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2

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

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

⊢ ∀x y. -x ≤ -y ⇔ y ≤ x

⊢ ∀x y. -x ≤ y ⇔ -y ≤ x

⊢ ∀x y. x ≤ -y ⇔ y ≤ -x

⊢ (∀x. 0 ≤ x ⇒ x ≠ −∞) ∧ ∀x. x ≤ 0 ⇒ x ≠ +∞

⊢ ∀n. 0 ≤ &n

⊢ ∀x. 0 ≤ x²

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x ≤ z + x ⇔ y ≤ z)

⊢ ∀x y z. y ≤ z ⇒ y + x ≤ z + x

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

⊢ ∀x. x ≤ x

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z ≤ y * z ⇔ x ≤ y)

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

⊢ ∀x y z. x ≤ y ⇒ x − z ≤ y − z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ −∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x

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

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

⊢ ∀p x. p x ⇒ x ≤ sup p

⊢ ∀p x. x ∈ p ⇒ x ≤ sup p

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

⊢ ∀x y. x ≤ y ∨ y ≤ x

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

⊢ ∀x y z. x ≤ y ∧ y = z ⇒ x ≤ z

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

⊢ ∀w x y z. w ≠ −∞ ∧ w ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

⊢ ∀w x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

⊢ ∀x y. ¬(x < y ∧ y ≤ x)

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

⊢ ∀x y. x ≤ y ∨ y < x

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

⊢ ∀f g l m.
    (f ⟶ l) sequentially ∧ (g ⟶ m) sequentially ⇒
    ((λx. f x + g x) ⟶ (l + m)) sequentially

⊢ ∀f l c.
    (∀n. f n ≠ +∞ ∧ f n ≠ −∞) ∧ l ≠ +∞ ∧ l ≠ −∞ ∧ c ≠ +∞ ∧ c ≠ −∞ ∧
    (f ⟶ l) sequentially ⇒
    ((λn. c * f n) ⟶ (c * l)) sequentially

⊢ ∀f l. (f ⟶ l) sequentially ⇒ (Normal ∘ f ⟶ Normal l) sequentially

⊢ ∀f l s.
    FINITE s ∧ (∀i. i ∈ s ⇒ (f i ⟶ l i) sequentially) ∧
    (∀i n. i ∈ s ⇒ f i n ≠ +∞ ∧ f i n ≠ −∞) ∧ (∀i. l i ≠ +∞ ∧ l i ≠ −∞) ⇒
    ((λn. ∑ (λi. f i n) s) ⟶ ∑ l s) sequentially

⊢ ∀x y. x * y = 1 ⇒ x = y⁻¹

⊢ ln 1 = 0

⊢ ∀x. 0 < x ⇒ ln x⁻¹ = -ln x

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ ln (x * y) = ln x + ln y

⊢ ∀x. 0 ≤ x ∧ x ≤ 1 ⇒ ln x ≤ 0

⊢ ∀x. 0 ≤ x ∧ x < 1 ⇒ ln x < 0

⊢ ∀x. 0 < x ⇒ ln x ≠ −∞

⊢ ∀x. 1 ≤ x ⇒ 0 ≤ ln x

⊢ ∀x. 1 < x ⇒ 0 < ln x

⊢ ∀x b. x ≠ −∞ ∧ x ≠ +∞ ⇒ logr b x ≠ −∞ ∧ logr b x ≠ +∞

⊢ 0 < 1

⊢ 0 < 2

⊢ -1 < 0

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

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

⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z

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

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y < x + y ⇔ 0 < x)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x < x + y ⇔ 0 < y)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y ⇒ x < x + y

⊢ ∀x y. ¬(x < y ∧ y < x)

⊢ ∀y z. 0 < y ∧ 0 < z ⇒ 0 < y / Normal z

⊢ ∀x y. x < y ⇒ x ≤ y

⊢ ∀x y. x < y ⇒ x ≠ y

⊢ ∀P e. 0 < e ∧ (∃x. P x ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. P x ∧ x < inf P + e

⊢ ∀P e.
    0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. x ∈ P ∧ x < inf P + e

⊢ ∀P e.
    0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. x ∈ P ∧ x < inf P + e

⊢ −∞ < +∞ ∧ (∀x. −∞ < Normal x ∧ Normal x < +∞) ∧
  (∀x. ¬(x < −∞) ∧ ¬(+∞ < x)) ∧ (∀x. x ≠ +∞ ⇔ x < +∞) ∧ ∀x. x ≠ −∞ ⇔ −∞ < x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y < x + z ⇔ y < z)

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

⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y < x * z ⇔ y < z)

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ∧ y < z ⇒ x * y < x * z

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ∧ y < z ⇒ x − z < x − y

⊢ ∀x y z. x < max y z ⇔ x < y ∨ x < z

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

⊢ ∀f x y n. x < max_fn_seq f n y ⇔ ∃i. i ≤ n ∧ x < f i y

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

⊢ ∀x1 x2 y1 y2.
    0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≠ +∞ ∧ y1 ≠ +∞ ∧ x1 < x2 ∧ y1 < y2 ⇒
    x1 * y1 < x2 * y2

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

⊢ ∀x y. -x < -y ⇔ y < x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x < z + x ⇔ y < z)

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

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

⊢ ∀x. ¬(x < x)

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z < y * z ⇔ x < y)

⊢ ∀x y z. x < y ∧ 0 < z ∧ z ≠ +∞ ⇒ x * z < y * z

⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ∧ x < y ⇒ x − z < y − z

⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)

⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)

⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀a s. a < sup s ⇔ ∃x. x ∈ s ∧ a < x

⊢ ∀x y. x = y ∨ x < y ∨ y < x

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

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

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

⊢ ∀x y. x < y ∨ y ≤ x

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

⊢ ∀x y. max x y = max y x

⊢ ∀g. max_fn_seq g 0 = g 0

⊢ ∀f x n. max_fn_seq f n x = sup (IMAGE (λi. f i x) (count (SUC n)))

⊢ (∀g x. max_fn_seq g 0 x = g 0 x) ∧
  (∀g n x.
     max_fn_seq g (NUMERAL (BIT1 n)) x =
     max (max_fn_seq g (NUMERAL (BIT1 n) − 1) x) (g (NUMERAL (BIT1 n)) x)) ∧
  ∀g n x.
    max_fn_seq g (NUMERAL (BIT2 n)) x =
    max (max_fn_seq g (NUMERAL (BIT1 n)) x) (g (NUMERAL (BIT2 n)) x)

⊢ ∀f g x. (∀n. f n x = g n x) ⇒ ∀n. max_fn_seq f n x = max_fn_seq g n x

⊢ ∀f x y n. max_fn_seq f n x ≤ y ⇔ ∀i. i ≤ n ⇒ f i x ≤ y

⊢ ∀g n x. max_fn_seq g n x ≤ max_fn_seq g (SUC n) x

⊢ ∀x. max x +∞ = +∞ ∧ max +∞ x = +∞ ∧ max −∞ x = x ∧ max x −∞ = x

⊢ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z

⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2

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

⊢ ∀x. max x x = x

⊢ ∀x y. min x y = min y x

⊢ ∀x. min x +∞ = x ∧ min +∞ x = x ∧ min −∞ x = −∞ ∧ min x −∞ = −∞

⊢ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z

⊢ ∀x y. min x y ≤ x

⊢ ∀x y. min x y ≤ y

⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2

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

⊢ ∀x. min x x = x

⊢ ∀f f'. mono_decreasing f ∧ (∀n. f n = Normal (f' n)) ⇒ mono_decreasing f'

⊢ ∀f. mono_decreasing f ⇒ mono_decreasing (Normal ∘ f)

⊢ ∀f f'. mono_increasing f ∧ (∀n. f n = Normal (f' n)) ⇒ mono_increasing f'

⊢ ∀f. mono_increasing f ⇒ mono_increasing (Normal ∘ f)

⊢ ∀f x0 y0.
    (∀x y. x ≤ y ⇒ f x ≤ f y) ∧ x0 < y0 ⇒
    inf {f x | Normal x0 < x} ≤ sup {f x | x < Normal y0}

⊢ monoidal $*

⊢ mspace extreal_mr1 = 𝕌(:extreal)

⊢ ∀x y z. x * (y * z) = x * y * z

⊢ ∀x y. x * y = y * x

⊢ ∀x r. r ≠ 0 ⇒ x = x * Normal r / Normal r

⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞

⊢ ∀x. x < 0 ⇒ +∞ * x = −∞ ∧ x * +∞ = −∞ ∧ −∞ * x = +∞ ∧ x * −∞ = +∞

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (x * y = x * z ⇔ x = 0 ∨ y = z)

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

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

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

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ * x = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x⁻¹ * x = 1

⊢ ∀x y. -x * y = -(x * y)

⊢ ∀x. 1 * x = x

⊢ ∀x. 0 < x ⇒ +∞ * x = +∞

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

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

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

⊢ ∀x. 0 * x = 0

⊢ (∀c y. 0 ≤ c ∧ y ≠ −∞ ⇒ Normal c * y ≠ −∞) ∧
  (∀c y. 0 ≤ c ∧ y ≠ +∞ ⇒ Normal c * y ≠ +∞) ∧
  (∀c y. c ≤ 0 ∧ y ≠ −∞ ⇒ Normal c * y ≠ +∞) ∧
  ∀c y. c ≤ 0 ∧ y ≠ +∞ ⇒ Normal c * y ≠ −∞

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ x * y ≠ −∞ ∧ x * y ≠ +∞

⊢ ∀x y a.
    0 ≤ x ∧ 0 ≤ y ∧ 0 < a ∧ a ≠ +∞ ⇒ (x * y) powr a = x powr a * y powr a

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (y * x = z * x ⇔ x = 0 ∨ y = z)

⊢ ∀x y. x * -y = -(x * y)

⊢ ∀x. x * 1 = x

⊢ ∀x. 0 < x ⇒ x * +∞ = +∞

⊢ ∀x. x * 0 = 0

⊢ 0 ≠ 1

⊢ 0 ≠ 2

⊢ -0 = 0

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -(x + y) = -x + -y

⊢ ∀x. -x = 0 ⇔ x = 0

⊢ ∀x. -x = -1 * x

⊢ ∀x y. -x * -y = x * y

⊢ ∀x. --x = x

⊢ ∀x. x ≤ 0 ⇒ x ≠ +∞

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∨ y ≠ −∞ ∧ y ≠ +∞ ⇒ -(x − y) = y − x

⊢ neutral $* = 1

⊢ ∀f. nonneg (abs ∘ f)

⊢ ∀f. nonneg f ⇒ abs ∘ f = f

⊢ ∀f. nonneg f ⇒ f⁻ = (λx. 0)

⊢ ∀f. nonneg f ⇒ f⁺ = f

⊢ Normal 0 = 0

⊢ Normal 1 = 1

⊢ ∀r. exp (Normal r) = Normal (exp r)

⊢ ∀s x. Normal (indicator s x) = 𝟙 s x

⊢ ∀x. x ≠ 0 ⇒ Normal x⁻¹ = (Normal x)⁻¹

⊢ Normal (-1) = -1

⊢ ∀c s x. Normal c * 𝟙 s x = Normal (c * indicator s x)

⊢ ∀r a. 0 < r ∧ 0 < a ⇒ Normal r powr Normal a = Normal (r powr a)

⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ Normal (real x) = x

⊢ ∀s. s ∩ IMAGE Normal 𝕌(:real) = IMAGE Normal (real_set s)

⊢ ∀n. &n < +∞

⊢ ∀n. &n ≠ −∞ ∧ &n ≠ +∞

⊢ ∀n. 1 pow n = 1

⊢ ∀a. 0 ≤ a ⇒ 1 powr a = 1

⊢ ∀a b c d.
    a < b ∧ c < d ⇒ (open_interval a b = open_interval c d ⇔ a = c ∧ b = d)

⊢ ∀x. 0 ≤ x ⇒ x ≠ −∞

⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃r. ∀n. ∑ f (count n) ≤ Normal r) ⇒ suminf f < +∞

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x² ≤ y²)

⊢ ∀x. 0 ≤ x ⇒ sqrt x² = x

⊢ ∀x. x pow 0 = 1

⊢ ∀x. x pow 1 = x

⊢ ∀x. x² = x * x

⊢ ∀x. x² = abs x * abs x

⊢ ∀c n. abs (c pow n) = abs c pow n

⊢ ∀x n m. x pow (n + m) = x pow n * x pow m

⊢ ∀n. EVEN n ⇒ ∀x. -x pow n = x pow n

⊢ ∀n. ODD n ⇒ ∀x. -x pow n = -(x pow n)

⊢ ∀n x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ (x / y) pow n = x pow n / y pow n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x = y ⇔ x pow n = y pow n)

⊢ ∀n. EVEN n ⇒ ∀x. 0 ≤ x pow n

⊢ ∀n. 0 ≤ (1 / 2) pow n

⊢ ∀n. 0 < (1 / 2) pow (n + 1)

⊢ suminf (λn. (1 / 2) pow (n + 1)) = 1

⊢ suminf (λn. (1 / 2) pow SUC n) = 1

⊢ ∀e. 0 < e ∧ e ≠ +∞ ⇒ e = suminf (λn. e * (1 / 2) pow (n + 1))

⊢ ∀n y. y ≠ 0 ⇒ (y pow n)⁻¹ = y⁻¹ pow n

⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x pow n ≤ y pow n)

⊢ ∀x n m. 1 ≤ x ∧ n ≤ m ⇒ x pow n ≤ x pow m

⊢ ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n

⊢ ∀n. -1 pow (2 * n) = 1

⊢ ∀n x y. (x * y) pow n = x pow n * y pow n

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

⊢ ∀n x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x pow n ≠ −∞ ∧ x pow n ≠ +∞

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

⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ x pow n

⊢ ∀n x. 0 < x ⇒ 0 < x pow n

⊢ ∀x m n. (x pow m) pow n = x pow (m * n)

⊢ ∀n x. x pow SUC n = 0 ⇔ x = 0

⊢ ∀n x. x pow n = 0 ⇒ x = 0

⊢ ∀x. x powr 0 = 1

⊢ ∀x. 0 ≤ x ⇒ x powr 1 = x

⊢ ∀a b c.
    0 ≤ a ∧ 0 ≤ b ∧ b ≠ +∞ ∧ 0 ≤ c ∧ c ≠ +∞ ⇒
    a powr (b + c) = a powr b * a powr c

⊢ ∀x a. 0 ≤ x ∧ 0 < a ∧ a ≠ +∞ ⇒ (x powr a = 0 ⇔ x = 0)

⊢ ∀a p. 1 ≤ a ∧ 0 ≤ p ⇒ 1 ≤ a powr p

⊢ ∀x. (1 < x ⇒ x powr +∞ = +∞) ∧ (x = 1 ⇒ x powr +∞ = 1) ∧
      (0 ≤ x ∧ x < 1 ⇒ x powr +∞ = 0)

⊢ ∀a b c. 1 < a ∧ a ≠ +∞ ∧ 0 ≤ b ∧ 0 ≤ c ⇒ (a powr b ≤ a powr c ⇔ b ≤ c)

⊢ ∀a b c. 0 ≤ a ∧ 0 ≤ c ∧ 0 < b ∧ b ≠ +∞ ⇒ (a powr b ≤ c powr b ⇔ a ≤ c)

⊢ ∀x a. 0 ≤ x powr a

⊢ ∀x a. 0 < x ∧ 0 ≤ a ∧ a ≠ +∞ ⇒ 0 < x powr a

⊢ ∀a b c.
    0 ≤ a ∧ 0 < b ∧ 0 < c ∧ b ≠ +∞ ∧ c ≠ +∞ ⇒
    (a powr b) powr c = a powr (b * c)

⊢ ∀n m. m ≠ 0 ⇒ &n / &m = Normal (&n / &m)

⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x = y / z ⇔ x * z = y)

⊢ real 0 = 0

⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r

⊢ ∀x. real (Normal x) = x

⊢ ∀s. real_set s = {real x | x ≠ +∞ ∧ x ≠ −∞ ∧ x ∈ s}

⊢ real_set ∅ = ∅

⊢ ∀f x0.
    (∀x y. x ≤ y ⇒ f x ≤ f y) ∧ f right_continuous_at Normal x0 ∧
    (∀x. f x ≠ +∞ ∧ f x ≠ −∞) ⇒
    ∀e. 0 < e ∧ e ≠ +∞ ⇒
        ∃d. 0 < d ∧ ∀x. x − x0 < d ⇒ f (Normal x) − f (Normal x0) ≤ e

⊢ ∀f. right_continuous f ⇔
      (∀x y. x ≤ y ⇒ f x ≤ f y) ∧
      ∀x. inf {f x' | Normal x < x'} = f (Normal x)

⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹

⊢ ∀x y f. (∀n. f n ≤ x) ∧ (f ⟶ y) sequentially ⇒ y ≤ x

⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ (f ⟶ x) sequentially ⇒ f n ≤ x

⊢ (∀P. seq_sup P 0 = @r. r ∈ P ∧ sup P < r + 1) ∧
  (∀P n.
     seq_sup P (NUMERAL (BIT1 n)) =
     @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT1 n)) ∧
         seq_sup P (NUMERAL (BIT1 n) − 1) < r ∧ r < sup P) ∧
  ∀P n.
    seq_sup P (NUMERAL (BIT2 n)) =
    @r. r ∈ P ∧ sup P < r + Normal ((1 / 2) pow NUMERAL (BIT2 n)) ∧
        seq_sup P (NUMERAL (BIT1 n)) < r ∧ r < sup P

⊢ sqrt 0 = 0

⊢ sqrt 1 = 1

⊢ ∀n. sqrt (&n) ≤ &n

⊢ ∀x. 1 ≤ x ⇒ sqrt x ≤ x

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

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (x * y) = sqrt x * sqrt y

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x

⊢ ∀x. 0 < x ⇒ 0 < sqrt x

⊢ ∀x. 0 < x ⇒ sqrt x ≠ 0

⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x

⊢ ∀x. 0 ≤ x ⇒ sqrt x = x powr 2⁻¹

⊢ ∀x. 0 ≤ x ⇒ real (sqrt x) = sqrt (real x)

⊢ ∀x y. x − y = 0 ⇒ x = y

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x − y + y = x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ x + (y − x) = y

⊢ ∀x r. x − Normal r + Normal r = x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ x = y ⇒ x − y = 0

⊢ (∀x. x ≠ −∞ ⇒ x − −∞ = +∞) ∧ (∀x. x ≠ +∞ ⇒ x − +∞ = −∞) ∧
  (∀x. x ≠ +∞ ⇒ +∞ − x = +∞) ∧ ∀x. x ≠ −∞ ⇒ −∞ − x = −∞

⊢ ∀x y z.
    x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
    x * (y − z) = x * y − x * z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ x ≠ −∞ ∧ z ≠ −∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z

⊢ ∀w x y z. w ≤ x ∧ z ≤ y ⇒ w − y ≤ x − z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x ≤ y ⇔ x − y ≤ 0)

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -x − y = -(x + y)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x < z ⇔ y < z + x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y < z + x ⇒ y − x < z

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y < z + x ⇒ y − x < z

⊢ ∀x y. x < y ⇒ x − y < 0

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ∧ x − y < 0 ⇒ x < y

⊢ ∀x. 0 − x = -x

⊢ ∀x y. (x ≠ −∞ ∧ y ≠ +∞ ⇒ x − y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y ≠ +∞)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y)² = x² + y² − 2 * x * y

⊢ ∀x y z.
    x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
    (x − y) * z = x * z − y * z

⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x − x = 0

⊢ ∀x y. x − -y = x + y

⊢ ∀x. x − 0 = x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ y ⇔ 0 ≤ y − x)

⊢ ∀x y. x < y ⇒ 0 < y − x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y − x ⇒ x < y

⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ suminf (Normal ∘ f) < +∞

⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ suminf (Normal ∘ f) = Normal (suminf f)

⊢ ∀f g.
    (∀n. 0 ≤ f n) ∧ (∀n. f n ≤ f (SUC n)) ∧ (∀n. 0 ≤ g n) ∧
    (∀n. g n ≤ g (SUC n)) ⇒
    sup (IMAGE (λn. f n + g n) 𝕌(:num)) =
    sup (IMAGE f 𝕌(:num)) + sup (IMAGE g 𝕌(:num))

⊢ ∀f g.
    ext_bounded (IMAGE f 𝕌(:num)) ∧ mono_increasing f ∧
    ext_bounded (IMAGE g 𝕌(:num)) ∧ mono_increasing g ⇒
    sup (IMAGE (λn. f n + g n) 𝕌(:num)) =
    sup (IMAGE f 𝕌(:num)) + sup (IMAGE g 𝕌(:num))

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ ∀m. abs (sup {a n | m ≤ n}) ≤ k

⊢ ∀a k. (∀n. abs (a n) ≤ k) ⇒ abs (sup (IMAGE a 𝕌(:α))) ≤ k

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

⊢ ∀e s. 0 < e ∧ abs (sup s) ≠ +∞ ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ sup s − e < x

⊢ ∀f c.
    0 ≤ c ⇒
    sup (IMAGE (λn. Normal c * f n) 𝕌(:α)) = Normal c * sup (IMAGE f 𝕌(:α))

⊢ ∀f c J.
    0 ≤ c ∧ J ≠ ∅ ⇒
    sup (IMAGE (λn. Normal c * f n) J) = Normal c * sup (IMAGE f J)

⊢ ∀f c.
    0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒
    sup (IMAGE (λn. c * f n) 𝕌(:α)) = c * sup (IMAGE f 𝕌(:α))

⊢ ∀f. sup {sup {f i j | j ∈ 𝕌(:num)} | i ∈ 𝕌(:num)} =
      sup {sup {f i j | i ∈ 𝕌(:num)} | j ∈ 𝕌(:num)}

⊢ ∀f A B.
    sup {sup {f i j | j ∈ A} | i ∈ B} = sup {sup {f i j | i ∈ B} | j ∈ A}

⊢ ∀x. sup (λy. y = x) = x

⊢ ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ x = z) ⇒ sup p = z

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

⊢ ∀s k. s ≠ ∅ ⇒ sup (IMAGE (λx. k) s) = k

⊢ ∀k. sup (IMAGE (λx. k) 𝕌(:α)) = k

⊢ ∀A. A ≠ ∅ ⇒ ∃f. IMAGE f 𝕌(:num) ⊆ A ∧ sup A = sup {f n | n ∈ 𝕌(:num)}

⊢ sup ∅ = −∞

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

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

⊢ ∀s. s ≠ ∅ ∧ bounded s ⇒ sup (IMAGE Normal s) = Normal (sup s)

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

⊢ ∀p x. sup p ≤ x ⇔ ∀y. p y ⇒ y ≤ x

⊢ ∀p x. sup p ≤ x ⇔ ∀y. y ∈ p ⇒ y ≤ x

⊢ ∀f z. (∀n. f n ≤ f (SUC n)) ∧ z < sup (IMAGE f 𝕌(:num)) ⇒ ∃n. z ≤ f n

⊢ ∀p q. (∀x. p x ⇒ ∃y. q y ∧ x ≤ y) ⇒ sup p ≤ sup q

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

⊢ ∀P y. (∃x. P x ∧ y < x) ⇔ y < sup P

⊢ ∀P y. (∃x. x ∈ P ∧ y < x) ⇔ y < sup P

⊢ ∀P e. 0 < e ∧ (∃x. P x ∧ x ≠ −∞) ∧ sup P ≠ +∞ ⇒ ∃x. P x ∧ sup P < x + e

⊢ ∀P e.
    0 < e ∧ (∃x. x ∈ P ∧ x ≠ −∞) ∧ sup P ≠ +∞ ⇒ ∃x. x ∈ P ∧ sup P < x + e

⊢ ∀p. sup p < +∞ ⇒ ∀x. p x ⇒ x < +∞

⊢ ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ sup p = z

⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ sup p ∈ p

⊢ ∀p q. (∀n. p n ≤ q n) ⇒ sup (IMAGE p 𝕌(:α)) ≤ sup (IMAGE q 𝕌(:α))

⊢ ∀f g A B.
    (∀n. n ∈ A ⇒ ∃m. m ∈ B ∧ f n ≤ g m) ⇒
    sup {f n | n ∈ A} ≤ sup {g n | n ∈ B}

⊢ ∀p q. p ⊆ q ⇒ sup p ≤ sup q

⊢ ∀s k. abs (sup s) ≤ Normal k ⇒ Normal (sup (s ∘ Normal)) = sup s

⊢ ∀s. ext_bounded s ∧ s ≠ ∅ ⇒ Normal (sup (s ∘ Normal)) = sup s

⊢ sup (λx. ∃n. x = &n) = +∞

⊢ ∀a b. a < b ⇒ sup (open_interval a b) = b

⊢ ∀a m. (∀n. 0 ≤ a n) ⇒ 0 ≤ sup {a n | m ≤ n}

⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ sup (IMAGE a 𝕌(:α))

⊢ ∀f l.
    mono_increasing f ⇒
    (f ⟶ l ⇔ sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)

⊢ ∀f l.
    mono_increasing f ⇒
    ((f ⟶ l) sequentially ⇔
     sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)

⊢ ∀A g.
    A ≠ ∅ ⇒
    ∃f. IMAGE f 𝕌(:num) ⊆ IMAGE g A ∧
        sup {g n | n ∈ A} = sup {f n | n ∈ 𝕌(:num)}

⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
      ∀N. sup (IMAGE (λn. f (n + N)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))

⊢ ∀a. sup {a} = a

⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
      sup (IMAGE (λn. f (SUC n)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))

⊢ ∀f s.
    FINITE s ∧ (∀i. i ∈ s ⇒ ∀n. 0 ≤ f i n) ∧
    (∀i. i ∈ s ⇒ ∀n. f i n ≤ f i (SUC n)) ⇒
    sup (IMAGE (λn. ∑ (λi. f i n) s) 𝕌(:num)) =
    ∑ (λi. sup (IMAGE (f i) 𝕌(:num))) s

⊢ sup 𝕌(:extreal) = +∞

⊢ 3 * (1 / 3) = 1

⊢ ((0 < 1 / 3 ∧ 1 / 3 < 1) ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧
  (0 ≤ 1 / 3 ∧ 1 / 3 ≤ 1) ∧ 0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1

⊢ topspace ext_euclidean = 𝕌(:extreal)

⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x

⊢ ∀a b p q.
    0 ≤ a ∧ 0 ≤ b ∧ 0 < p ∧ 0 < q ∧ p ≠ +∞ ∧ q ≠ +∞ ∧ p⁻¹ + q⁻¹ = 1 ⇒
    a * b ≤ a powr p / p + b powr q / q

⊢ ∀x. x ≠ 0 ⇒ 0 / x = 0

⊢ ∀n. 0 < n ⇒ 0 pow n = 0

⊢ ∀x. 0 < x ⇒ 0 powr x = 0