Theory "extreal"

Signature

Definitions

EXTREAL_PROD_IMAGE_DEF

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

EXTREAL_SUM_IMAGE_DEF

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

Q_set_def

⊢ ℚ =
  {x | ∃a b. (x = &a / &b) ∧ 0 < &b} ∪ {x | ∃a b. (x = -(&a / &b)) ∧ 0 < &b}

ceiling_def

⊢ ∀x. ceiling (Normal x) = LEAST n. x ≤ &n

ext_liminf_def

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

ext_limsup_def

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

ext_mono_decreasing_def

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

ext_mono_increasing_def

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

ext_suminf_def

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

extreal_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('extreal').
             (∀a0.
                (a0 = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM)) ∨
                (a0 = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
                (∃a. a0 =
                     (λa.
                          ind_type$CONSTR (SUC (SUC 0)) a
                            (λn. ind_type$BOTTOM)) a) ⇒
                $var$('extreal') a0) ⇒
             $var$('extreal') a0) rep

extreal_abs_primitive_def

⊢ abs =
  WFREC (@R. WF R)
    (λextreal_abs a.
         case a of −∞ => I +∞ | +∞ => I +∞ | Normal x => I (Normal (abs x)))

extreal_ainv_def

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

extreal_case_def

⊢ (∀v v1 f. extreal_CASE −∞ v v1 f = v) ∧
  (∀v v1 f. extreal_CASE +∞ v v1 f = v1) ∧
  ∀a v v1 f. extreal_CASE (Normal a) v v1 f = f a

extreal_div_def

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

extreal_exp_def

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

extreal_inf_def

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

extreal_inv_def

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

extreal_lg_def

⊢ ∀x. lg x = logr 2 x

extreal_ln_def

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

extreal_logr_def

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

extreal_lt_def

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

extreal_max_def

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

extreal_min_def

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

extreal_of_num_def

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

extreal_pow_def

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

extreal_powr_def

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

extreal_size_def

⊢ (extreal_size −∞ = 0) ∧ (extreal_size +∞ = 0) ∧
  ∀a. extreal_size (Normal a) = 1

extreal_sqrt_def

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

extreal_sup_def

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

max_fn_seq_def

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

open_interval_def

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

open_intervals_def

⊢ open_intervals = {open_interval a b | T}

rational_intervals_def

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

real_def

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

real_set_def

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

seq_sup_def

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

Theorems

ABS_LE_HALF_POW2

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

ADD_IN_Q

⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x + y ∈ ℚ

CEILING_LBOUND

⊢ ∀x. Normal x ≤ &ceiling (Normal x)

CEILING_UBOUND

⊢ ∀x. 0 ≤ x ⇒ &ceiling (Normal x) < Normal x + 1

CMUL_IN_Q

⊢ ∀z x. x ∈ ℚ ⇒ &z * x ∈ ℚ ∧ -&z * x ∈ ℚ

COUNTABLE_ENUM_Q

⊢ ∀c. COUNTABLE c ⇔ (c = ∅) ∨ ∃f. c = IMAGE f ℚ

COUNTABLE_RATIONAL_INTERVALS

⊢ COUNTABLE rational_intervals

CROSS_COUNTABLE_UNIV

⊢ COUNTABLE (𝕌(:num) × 𝕌(:num))

DIV_IN_Q

⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ∧ y ≠ 0 ⇒ x / y ∈ ℚ

EXTREAL_ARCH

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

EXTREAL_ARCH_POW

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

EXTREAL_ARCH_POW_INV

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

EXTREAL_EQ_LADD

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

EXTREAL_EQ_RADD

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

EXTREAL_PROD_IMAGE_DISJOINT_UNION

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

EXTREAL_PROD_IMAGE_EMPTY

⊢ ∀f. ∏ f ∅ = 1

EXTREAL_PROD_IMAGE_EQ

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

EXTREAL_PROD_IMAGE_IMAGE

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

EXTREAL_PROD_IMAGE_PAIR

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

EXTREAL_PROD_IMAGE_PROPERTY

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

EXTREAL_PROD_IMAGE_SING

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

EXTREAL_PROD_IMAGE_THM

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

EXTREAL_SUM_IMAGE_0

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

EXTREAL_SUM_IMAGE_ADD

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

EXTREAL_SUM_IMAGE_CMUL

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

EXTREAL_SUM_IMAGE_COUNT

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

EXTREAL_SUM_IMAGE_DISJOINT_UNION

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

EXTREAL_SUM_IMAGE_EMPTY

⊢ ∀f. ∑ f ∅ = 0

EXTREAL_SUM_IMAGE_EQ

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

EXTREAL_SUM_IMAGE_EQ_CARD

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

EXTREAL_SUM_IMAGE_FINITE_CONST

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

EXTREAL_SUM_IMAGE_FINITE_SAME

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

EXTREAL_SUM_IMAGE_IF_ELIM

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

EXTREAL_SUM_IMAGE_IMAGE

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

EXTREAL_SUM_IMAGE_INSERT

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

EXTREAL_SUM_IMAGE_INTER_ELIM

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

EXTREAL_SUM_IMAGE_INTER_NONZERO

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

EXTREAL_SUM_IMAGE_INV_CARD_EQ_1

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

EXTREAL_SUM_IMAGE_IN_IF

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

EXTREAL_SUM_IMAGE_IN_IF_ALT

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

EXTREAL_SUM_IMAGE_MONO

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

EXTREAL_SUM_IMAGE_MONO_SET

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

EXTREAL_SUM_IMAGE_NEG

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

EXTREAL_SUM_IMAGE_NORMAL

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

EXTREAL_SUM_IMAGE_NOT_INFTY

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

EXTREAL_SUM_IMAGE_NOT_NEGINF

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

EXTREAL_SUM_IMAGE_NOT_POSINF

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

EXTREAL_SUM_IMAGE_PERMUTES

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

EXTREAL_SUM_IMAGE_POS

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

EXTREAL_SUM_IMAGE_POS_MEM_LE

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

EXTREAL_SUM_IMAGE_POW

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

EXTREAL_SUM_IMAGE_PROPERTY

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

EXTREAL_SUM_IMAGE_PROPERTY_NEG

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

EXTREAL_SUM_IMAGE_PROPERTY_POS

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

EXTREAL_SUM_IMAGE_SING

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

EXTREAL_SUM_IMAGE_SNEG

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

EXTREAL_SUM_IMAGE_SPOS

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

EXTREAL_SUM_IMAGE_SUB

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

EXTREAL_SUM_IMAGE_SUM_IMAGE

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

EXTREAL_SUM_IMAGE_SUM_IMAGE_MONO

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

EXTREAL_SUM_IMAGE_THM

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

EXTREAL_SUM_IMAGE_ZERO

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

EXTREAL_SUM_IMAGE_ZERO_DIFF

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

EXTREAL_SUM_IMAGE_le_suminf

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

EXTREAL_SUP_FUN_SEQ_IMAGE

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

EXTREAL_SUP_FUN_SEQ_MONO_IMAGE

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

EXTREAL_SUP_SEQ

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

INV_IN_Q

⊢ ∀x. x ∈ ℚ ∧ x ≠ 0 ⇒ 1 / x ∈ ℚ

MUL_IN_Q

⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x * y ∈ ℚ

NESTED_EXTREAL_SUM_IMAGE_REVERSE

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

NUM_IN_Q

⊢ ∀n. &n ∈ ℚ ∧ -&n ∈ ℚ

OPP_IN_Q

⊢ ∀x. x ∈ ℚ ⇒ -x ∈ ℚ

Q_COUNTABLE

⊢ COUNTABLE ℚ

Q_DENSE_IN_R

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

Q_DENSE_IN_R_LEMMA

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

Q_INFINITE

⊢ INFINITE ℚ

Q_not_infty

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

REAL_LE_MUL_EPSILON

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

REAL_LE_RSUB_GE0

⊢ ∀x y. x ≤ y ⇔ 0 ≤ y − x

SIMP_EXTREAL_ARCH

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

SIMP_EXTREAL_ARCH_NEG

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

SUB_IN_Q

⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x − y ∈ ℚ

abs_0

⊢ abs 0 = 0

abs_abs

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

abs_bounds

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

abs_bounds_lt

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

abs_div

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

abs_eq_0

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

abs_gt_0

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

abs_le_0

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

abs_le_half_pow2

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

abs_le_square_plus1

⊢ ∀x. abs x ≤ x² + 1

abs_max

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

abs_mul

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

abs_neg

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

abs_not_infty

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

abs_pos

⊢ ∀x. 0 ≤ abs x

abs_pow2

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

abs_pow_le_mono

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

abs_refl

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

abs_triangle

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

abs_triangle_sub

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

abs_unbounds

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

add2_sub2

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

add_assoc

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

add_comm

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

add_comm_normal

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

add_infty

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

add_ldistrib

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

add_ldistrib_neg

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

add_ldistrib_normal

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

add_ldistrib_normal2

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

add_ldistrib_pos

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

add_lzero

⊢ ∀x. 0 + x = x

add_not_infty

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

add_pow2

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

add_pow2_pos

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

add_rdistrib

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

add_rdistrib_normal

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

add_rdistrib_normal2

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

add_rzero

⊢ ∀x. x + 0 = x

add_sub

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

add_sub2

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

datatype_extreal

⊢ DATATYPE (extreal −∞ +∞ Normal)

div_add

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

div_add2

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

div_eq_mul_linv

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

div_infty

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

div_mul_refl

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

div_not_infty

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

div_one

⊢ ∀x. x / 1 = x

div_refl

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

div_refl_pos

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

entire

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

eq_add_sub_switch

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

eq_neg

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

eq_sub_ladd

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

eq_sub_ladd_normal

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

eq_sub_radd

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

eq_sub_switch

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

exp_0

⊢ exp 0 = 1

exp_pos

⊢ ∀x. 0 ≤ exp x

ext_mono_decreasing_suc

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

ext_mono_increasing_suc

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

ext_suminf_0

⊢ suminf (λn. 0) = 0

ext_suminf_2d

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

ext_suminf_2d_full

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

ext_suminf_add

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

ext_suminf_alt

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

ext_suminf_alt'

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

ext_suminf_cmul

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

ext_suminf_cmul_alt

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

ext_suminf_eq

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

ext_suminf_eq_infty

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

ext_suminf_eq_infty_imp

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

ext_suminf_lt_infty

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

ext_suminf_mono

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

ext_suminf_pos

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

ext_suminf_posinf

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

ext_suminf_real_suminf

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

ext_suminf_sigma

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

ext_suminf_sigma'

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

ext_suminf_sing

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

ext_suminf_sub

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

ext_suminf_sum

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

ext_suminf_suminf

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

ext_suminf_suminf'

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

ext_suminf_summable

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

ext_suminf_sup_eq

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

ext_suminf_zero

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

extreal_11

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

extreal_Axiom

⊢ ∀f0 f1 f2. ∃fn. (fn −∞ = f0) ∧ (fn +∞ = f1) ∧ ∀a. fn (Normal a) = f2 a

extreal_abs_def

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

extreal_abs_ind

⊢ ∀P. (∀x. P (Normal x)) ∧ P −∞ ∧ P +∞ ⇒ ∀v. P v

extreal_add_def

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

extreal_add_eq

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

extreal_add_ind

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

extreal_case_cong

⊢ ∀M M' v v1 f.
    (M = M') ∧ ((M' = −∞) ⇒ (v = v')) ∧ ((M' = +∞) ⇒ (v1 = v1')) ∧
    (∀a. (M' = Normal a) ⇒ (f a = f' a)) ⇒
    (extreal_CASE M v v1 f = extreal_CASE M' v' v1' f')

extreal_case_eq

⊢ (extreal_CASE x v v1 f = v') ⇔
  (x = −∞) ∧ (v = v') ∨ (x = +∞) ∧ (v1 = v') ∨ ∃r. (x = Normal r) ∧ (f r = v')

extreal_cases

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

extreal_distinct

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

extreal_div_eq

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

extreal_eq_zero

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

extreal_induction

⊢ ∀P. P −∞ ∧ P +∞ ∧ (∀r. P (Normal r)) ⇒ ∀e. P e

extreal_inv_eq

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

extreal_le_def

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

extreal_le_eq

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

extreal_le_ind

⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P −∞ v0) ∧ P +∞ +∞ ∧
      (∀v5. P (Normal v5) +∞) ∧ P +∞ −∞ ∧ (∀v6. P (Normal v6) −∞) ∧
      (∀v8. P +∞ (Normal v8)) ⇒
      ∀v v1. P v v1

extreal_lt_eq

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

extreal_mean

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

extreal_mul_def

⊢ (−∞ * −∞ = +∞) ∧ (−∞ * +∞ = −∞) ∧ (+∞ * −∞ = −∞) ∧ (+∞ * +∞ = +∞) ∧
  (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))

extreal_mul_ind

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

extreal_nchotomy

⊢ ∀ee. (ee = −∞) ∨ (ee = +∞) ∨ ∃r. ee = Normal r

extreal_not_infty

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

extreal_not_lt

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

extreal_sub_add

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

extreal_sub_def

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

extreal_sub_eq

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

extreal_sub_ind

⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P −∞ (Normal v0)) ∧
      (∀v0. P +∞ (Normal v0)) ∧ (∀v1. P (Normal v1) −∞) ∧
      (∀v2. P (Normal v2) +∞) ∧ P −∞ +∞ ∧ P +∞ −∞ ∧ P −∞ −∞ ∧ P +∞ +∞ ⇒
      ∀v v1. P v v1

fourth_cancel

⊢ 4 * (1 / 4) = 1

fourths_between

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

gen_powr

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

half_between

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

half_cancel

⊢ 2 * (1 / 2) = 1

half_not_infty

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

harmonic_series_pow_2

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

inf_cminus

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

inf_const

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

inf_const_alt

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

inf_const_over_set

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

inf_empty

⊢ inf ∅ = +∞

inf_eq

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

inf_eq'

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

inf_le

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

inf_le'

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

inf_le_imp

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

inf_le_imp'

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

inf_lt

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

inf_lt'

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

inf_lt_infty

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

inf_min

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

inf_minimal

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

inf_mono_subset

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

inf_seq

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

inf_sing

⊢ ∀a. inf {a} = a

inf_suc

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

inf_univ

⊢ inf 𝕌(:extreal) = −∞

infty_div

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

inv_1over

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

inv_inj

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

inv_le_antimono

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

inv_lt_antimono

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

inv_mul

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

inv_not_infty

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

inv_one

⊢ 1⁻¹ = 1

inv_pos

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

inv_pos'

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

inv_pos_eq

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

ldiv_eq

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

ldiv_le_imp

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

le_01

⊢ 0 ≤ 1

le_02

⊢ 0 ≤ 2

le_abs

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

le_abs_bounds

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

le_add

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

le_add2

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

le_add_neg

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

le_addl_imp

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

le_addr

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

le_addr_imp

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

le_antisym

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

le_div

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

le_epsilon

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

le_inf

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

le_inf'

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

le_inf_epsilon_set

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

le_infty

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

le_inv

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

le_ladd

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

le_ladd_imp

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

le_ldiv

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

le_lmul_imp

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

le_lneg

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

le_lsub_imp

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

le_lt

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

le_max

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

le_max1

⊢ ∀x y. x ≤ max x y

le_max2

⊢ ∀x y. y ≤ max x y

le_min

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

le_mul

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

le_mul_epsilon

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

le_mul_neg

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

le_neg

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

le_not_infty

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

le_num

⊢ ∀n. 0 ≤ &n

le_pow2

⊢ ∀x. 0 ≤ x²

le_radd

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

le_radd_imp

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

le_rdiv

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

le_refl

⊢ ∀x. x ≤ x

le_rmul_imp

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

le_rsub_imp

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

le_sub_eq

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

le_sub_eq2

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

le_sub_imp

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

le_sub_imp2

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

le_sup

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

le_sup'

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

le_sup_imp

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

le_sup_imp'

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

le_sup_imp2

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

le_total

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

le_trans

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

let_add

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

let_add2

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

let_add2_alt

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

let_antisym

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

let_mul

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

let_total

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

let_trans

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

linv_uniq

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

logr_not_infty

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

lt_01

⊢ 0 < 1

lt_02

⊢ 0 < 2

lt_10

⊢ -1 < 0

lt_abs_bounds

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

lt_add

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

lt_add2

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

lt_add_neg

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

lt_addl

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

lt_addr_imp

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

lt_antisym

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

lt_div

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

lt_imp_le

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

lt_imp_ne

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

lt_inf_epsilon

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

lt_inf_epsilon_set

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

lt_infty

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

lt_ladd

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

lt_ldiv

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

lt_le

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

lt_lmul

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

lt_max_between

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

lt_mul

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

lt_mul2

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

lt_mul_neg

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

lt_neg

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

lt_radd

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

lt_rdiv

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

lt_rdiv_neg

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

lt_refl

⊢ ∀x. ¬(x < x)

lt_rmul

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

lt_sub

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

lt_sub'

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

lt_sub_imp

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

lt_sub_imp'

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

lt_sub_imp2

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

lt_sup

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

lt_total

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

lt_trans

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

lte_add

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

lte_mul

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

lte_total

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

lte_trans

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

max_comm

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

max_fn_seq_compute

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

max_fn_seq_mono

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

max_infty

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

max_le

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

max_le2_imp

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

max_reduce

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

max_refl

⊢ ∀x. max x x = x

min_comm

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

min_infty

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

min_le

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

min_le1

⊢ ∀x y. min x y ≤ x

min_le2

⊢ ∀x y. min x y ≤ y

min_le2_imp

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

min_le_between

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

min_reduce

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

min_refl

⊢ ∀x. min x x = x

mul_assoc

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

mul_comm

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

mul_div_refl

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

mul_infty

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

mul_lcancel

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

mul_le

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

mul_le2

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

mul_let

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

mul_linv

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

mul_linv_pos

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

mul_lneg

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

mul_lone

⊢ ∀x. 1 * x = x

mul_lposinf

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

mul_lt

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

mul_lt2

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

mul_lte

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

mul_lzero

⊢ ∀x. 0 * x = 0

mul_not_infty

⊢ (∀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 ≠ −∞

mul_not_infty2

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

mul_rneg

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

mul_rone

⊢ ∀x. x * 1 = x

mul_rposinf

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

mul_rzero

⊢ ∀x. x * 0 = 0

ne_01

⊢ 0 ≠ 1

ne_02

⊢ 0 ≠ 2

neg_0

⊢ -0 = 0

neg_add

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

neg_eq0

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

neg_minus1

⊢ ∀x. -x = -1 * x

neg_mul2

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

neg_neg

⊢ ∀x. - -x = x

neg_not_posinf

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

neg_sub

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

normal_exp

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

normal_inv_eq

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

normal_powr

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

normal_real

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

normal_real_set

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

num_lt_infty

⊢ ∀n. &n < +∞

num_not_infty

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

one_pow

⊢ ∀n. 1 pow n = 1

pos_not_neginf

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

pos_summable

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

pow2_le_eq

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

pow2_sqrt

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

pow_0

⊢ ∀x. x pow 0 = 1

pow_1

⊢ ∀x. x pow 1 = x

pow_2

⊢ ∀x. x² = x * x

pow_add

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

pow_div

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

pow_half_pos_le

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

pow_half_pos_lt

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

pow_half_ser

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

pow_half_ser'

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

pow_half_ser_by_e

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

pow_inv

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

pow_le

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

pow_le_full

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

pow_le_mono

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

pow_lt

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

pow_lt2

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

pow_minus1

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

pow_mul

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

pow_neg_odd

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

pow_not_infty

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

pow_pos_even

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

pow_pos_le

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

pow_pos_lt

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

pow_zero

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

pow_zero_imp

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

powr_0

⊢ ∀x. x powr 0 = 1

powr_pos

⊢ ∀x a. 0 ≤ x powr a

quotient_normal

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

rat_not_infty

⊢ ∀r. r ∈ ℚ ⇒ r ≠ −∞ ∧ r ≠ +∞

rdiv_eq

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

real_normal

⊢ ∀x. real (Normal x) = x

rinv_uniq

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

seq_sup_compute

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

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

sqrt_pos_le

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

sqrt_pos_lt

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

sqrt_pow2

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

sub_0

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

sub_add

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

sub_add2

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

sub_eq_0

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

sub_infty

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

sub_ldistrib

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

sub_le_eq

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

sub_le_eq2

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

sub_le_imp

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

sub_le_imp2

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

sub_le_switch

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

sub_le_switch2

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

sub_le_zero

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

sub_lneg

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

sub_lt_eq

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

sub_lt_imp

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

sub_lt_imp2

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

sub_lt_zero

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

sub_lt_zero2

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

sub_lzero

⊢ ∀x. 0 − x = -x

sub_not_infty

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

sub_pow2

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

sub_rdistrib

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

sub_refl

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

sub_rneg

⊢ ∀c x. Normal c − -x = Normal c + x

sub_rzero

⊢ ∀x. x − 0 = x

sub_zero_le

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

sub_zero_lt

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

sub_zero_lt2

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

summable_ext_suminf

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

summable_ext_suminf_suminf

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

sup_add_mono

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

sup_close

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

sup_cmul

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

sup_cmult

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

sup_comm

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

sup_const

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

sup_const_alt

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

sup_const_alt'

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

sup_const_over_set

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

sup_const_over_univ

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

sup_countable_seq

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

sup_empty

⊢ sup ∅ = −∞

sup_eq

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

sup_eq'

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

sup_le

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

sup_le'

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

sup_le_mono

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

sup_le_sup_imp

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

sup_le_sup_imp'

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

sup_lt

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

sup_lt'

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

sup_lt_epsilon

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

sup_lt_infty

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

sup_max

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

sup_maximal

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

sup_mono

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

sup_mono_ext

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

sup_mono_subset

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

sup_num

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

sup_seq

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

sup_seq_countable_seq

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

sup_shift

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

sup_sing

⊢ ∀a. sup {a} = a

sup_suc

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

sup_sum_mono

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

⊢ sup 𝕌(:extreal) = +∞

third_cancel

⊢ 3 * (1 / 3) = 1

thirds_between

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

zero_div

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

zero_pow

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

zero_rpow

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