Theory "extreal"

Signature

Definitions

real_def

⊢ ∀x. real x = if (x = NegInf) ∨ (x = PosInf) then 0 else @r. x = Normal r

rational_intervals_def

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

Q_set_def

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

open_intervals_set_def

⊢ open_intervals_set = {open_interval a b | a ∈ 𝕌(:extreal) ∧ b ∈ 𝕌(:extreal)}

open_interval_def

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

mono_increasing_def

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

mono_decreasing_def

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

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_sup_def

⊢ ∀p.
      sup p =
      if ∀x. (∀y. p y ⇒ y ≤ x) ⇒ (x = PosInf) then PosInf
      else if ∀x. p x ⇒ (x = NegInf) then NegInf
      else Normal (sup (λr. p (Normal r)))

EXTREAL_SUM_IMAGE_DEF

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

extreal_sqrt_def

⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ (sqrt PosInf = PosInf)

extreal_size_def

⊢ (extreal_size NegInf = 0) ∧ (extreal_size PosInf = 0) ∧
  ∀a. extreal_size (Normal a) = 1

extreal_pow_def

⊢ (∀a n. Normal a pow n = Normal (a pow n)) ∧
  (∀n. PosInf pow n = if n = 0 then Normal 1 else PosInf) ∧
  ∀n.
      NegInf pow n =
      if n = 0 then Normal 1 else if EVEN n then PosInf else NegInf

extreal_of_num_def

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

extreal_min_def

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

extreal_max_def

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

extreal_lt_def

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

extreal_logr_def

⊢ (∀b x. logr b (Normal x) = Normal (logr b x)) ∧
  (∀b. logr b PosInf = PosInf) ∧ ∀b. logr b NegInf = NegInf

extreal_lg_def

⊢ ∀x. lg x = logr 2 x

extreal_inv_def

⊢ (inv NegInf = Normal 0) ∧ (inv PosInf = Normal 0) ∧
  ∀x. inv (Normal x) = Normal x⁻¹

extreal_inf_def

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

extreal_exp_def

⊢ (∀x. exp (Normal x) = Normal (exp x)) ∧ (exp PosInf = PosInf) ∧
  (exp NegInf = Normal 0)

extreal_div_def

⊢ ∀x y. x / y = x * inv y

extreal_case_def

⊢ (∀v v1 f. extreal_CASE NegInf v v1 f = v) ∧
  (∀v v1 f. extreal_CASE PosInf v v1 f = v1) ∧
  ∀a v v1 f. extreal_CASE (Normal a) v v1 f = f a

extreal_ainv_def

⊢ (-NegInf = PosInf) ∧ (-PosInf = NegInf) ∧ ∀x. -Normal x = Normal (-x)

extreal_abs_primitive_def

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

ext_suminf_def

⊢ ∀f. suminf f = sup (IMAGE (λn. SIGMA f (count n)) 𝕌(:num))

ext_mono_increasing_def

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

ext_mono_decreasing_def

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

ceiling_def

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

Theorems

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

third_cancel

⊢ 3 * (1 / 3) = 1

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. SIGMA (λi. f i n) s) 𝕌(:num)) =
       SIGMA (λi. sup (IMAGE (f i) 𝕌(:num))) s)

sup_suc

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

sup_seq

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

sup_num

⊢ sup (λx. ∃n. x = &n) = PosInf

sup_mono

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

sup_max

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

sup_lt_infty

⊢ ∀p. sup p < PosInf ⇒ ∀x. p x ⇒ x < PosInf

sup_lt_epsilon

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

sup_lt

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

sup_le_sup_imp

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

sup_le_mono

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

sup_le

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

sup_eq

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

sup_const_over_set

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

sup_const_alt

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

sup_const

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

sup_cmul

⊢ ∀f c.
      0 ≤ c ⇒
      (sup (IMAGE (λn. Normal c * f n) 𝕌(:α)) = Normal c * sup (IMAGE 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)))

sub_zero_lt2

⊢ ∀x y. x ≠ NegInf ∧ x ≠ PosInf ∧ 0 < y − x ⇒ x < y

sub_zero_lt

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

sub_zero_le

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

sub_rzero

⊢ ∀x. x − 0 = x

sub_rneg

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

sub_refl

⊢ ∀x. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x − x = 0)

sub_rdistrib

⊢ ∀x y z.
      x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ∧ z ≠ NegInf ∧
      z ≠ PosInf ⇒
      ((x − y) * z = x * z − y * z)

sub_not_infty

⊢ ∀x y.
      (x ≠ NegInf ∧ y ≠ PosInf ⇒ x − y ≠ NegInf) ∧
      (x ≠ PosInf ∧ y ≠ NegInf ⇒ x − y ≠ PosInf)

sub_lzero

⊢ ∀x. 0 − x = -x

sub_lt_zero2

⊢ ∀x y. y ≠ NegInf ∧ y ≠ PosInf ∧ x − y < 0 ⇒ x < y

sub_lt_zero

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

sub_lt_imp2

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

sub_lt_imp

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

sub_lneg

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

sub_le_zero

⊢ ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (x ≤ y ⇔ x − y ≤ 0)

sub_le_switch2

⊢ ∀x y z.
      x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ⇒
      (y − x ≤ z ⇔ y − z ≤ x)

sub_le_switch

⊢ ∀x y z.
      x ≠ NegInf ∧ x ≠ PosInf ∧ z ≠ NegInf ∧ z ≠ PosInf ⇒
      (y − x ≤ z ⇔ y − z ≤ x)

sub_le_imp2

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

sub_le_imp

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

sub_le_eq2

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

sub_le_eq

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

sub_ldistrib

⊢ ∀x y z.
      x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ∧ z ≠ NegInf ∧
      z ≠ PosInf ⇒
      (x * (y − z) = x * y − x * z)

SUB_IN_Q

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

sub_add2

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

sub_add

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

sub_0

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

sqrt_pow2

⊢ ∀x. (sqrt x pow 2 = x) ⇔ 0 ≤ x

sqrt_pos_lt

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

sqrt_pos_le

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

sqrt_mono_le

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

SIMP_REAL_ARCH_NEG

⊢ ∀x. ∃n. -&n ≤ x

SIMP_REAL_ARCH

⊢ ∀x. ∃n. x ≤ &n

SIMP_EXTREAL_ARCH

⊢ ∀x. x ≠ PosInf ⇒ ∃n. x ≤ &n

rinv_uniq

⊢ ∀x y. (x * y = 1) ⇒ (y = inv x)

real_normal

⊢ ∀x. real (Normal x) = x

REAL_LT_RMUL_NEG_0_NEG

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

REAL_LT_RMUL_NEG_0

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

REAL_LT_RMUL_0_NEG

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

REAL_LT_RDIV_EQ_NEG

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

REAL_LT_LMUL_NEG_0_NEG

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

REAL_LT_LMUL_NEG_0

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

REAL_LT_LMUL_0_NEG

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

REAL_LE_RDIV_EQ_NEG

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

REAL_LE_MUL_EPSILON

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

REAL_ARCH_POW

⊢ ∀x. ∃n. x < 2 pow n

rat_not_infty

⊢ ∀r. r ∈ Q_set ⇒ r ≠ NegInf ∧ r ≠ PosInf

quotient_normal

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

Q_not_infty

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

Q_INFINITE

⊢ INFINITE Q_set

Q_DENSE_IN_R_LEMMA

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

Q_DENSE_IN_R

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

Q_COUNTABLE

⊢ COUNTABLE Q_set

pow_zero_imp

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

pow_zero

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

pow_pos_lt

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

pow_pos_le

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

pow_pos_even

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

POW_POS_EVEN

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

pow_not_infty

⊢ ∀n x. x ≠ NegInf ∧ x ≠ PosInf ⇒ x pow n ≠ NegInf ∧ x pow n ≠ PosInf

pow_neg_odd

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

POW_NEG_ODD

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

pow_mul

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

pow_minus1

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

pow_lt2

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

pow_lt

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

pow_le_mono

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

pow_le

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

pow_add

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

pow_2

⊢ ∀x. x pow 2 = x * x

pow_1

⊢ ∀x. x pow 1 = x

pow_0

⊢ ∀x. x pow 0 = 1

pow2_sqrt

⊢ ∀x. 0 ≤ x ⇒ (sqrt (x pow 2) = x)

OPP_IN_Q

⊢ ∀x. x ∈ Q_set ⇒ -x ∈ Q_set

num_not_infty

⊢ ∀n. &n ≠ NegInf ∧ &n ≠ PosInf

NUM_IN_Q

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

normal_real

⊢ ∀x. x ≠ NegInf ∧ x ≠ PosInf ⇒ (Normal (real x) = x)

neg_sub

⊢ ∀x y. x ≠ NegInf ∧ x ≠ PosInf ∨ y ≠ NegInf ∧ y ≠ PosInf ⇒ (-(x − y) = y − x)

neg_neg

⊢ ∀x. - -x = x

neg_mul2

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

neg_minus1

⊢ ∀x. -x = -1 * x

neg_eq0

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

neg_0

⊢ -0 = 0

ne_02

⊢ 0 ≠ 2

ne_01

⊢ 0 ≠ 1

mul_rzero

⊢ ∀x. x * 0 = 0

mul_rone

⊢ ∀x. x * 1 = x

mul_rneg

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

mul_not_infty2

⊢ ∀x y.
      x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ⇒
      x * y ≠ NegInf ∧ x * y ≠ PosInf

mul_not_infty

⊢ (∀c y. 0 ≤ c ∧ y ≠ NegInf ⇒ Normal c * y ≠ NegInf) ∧
  (∀c y. 0 ≤ c ∧ y ≠ PosInf ⇒ Normal c * y ≠ PosInf) ∧
  (∀c y. c ≤ 0 ∧ y ≠ NegInf ⇒ Normal c * y ≠ PosInf) ∧
  ∀c y. c ≤ 0 ∧ y ≠ PosInf ⇒ Normal c * y ≠ NegInf

mul_lzero

⊢ ∀x. 0 * x = 0

mul_lte

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

mul_lt

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

mul_lone

⊢ ∀x. 1 * x = x

mul_lneg

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

mul_let

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

mul_le

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

MUL_IN_Q

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

mul_comm

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

mul_assoc

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

mono_increasing_suc

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

mono_increasing_converges_to_sup

⊢ ∀f r. mono_increasing f ∧ f --> r ⇒ (r = sup (IMAGE f 𝕌(:num)))

mono_decreasing_suc

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

min_refl

⊢ ∀x. min x x = x

min_le2_imp

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

min_le2

⊢ ∀x y. min x y ≤ y

min_le1

⊢ ∀x y. min x y ≤ x

min_le

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

min_infty

⊢ ∀x.
      (min x PosInf = x) ∧ (min PosInf x = x) ∧ (min NegInf x = NegInf) ∧
      (min x NegInf = NegInf)

min_comm

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

max_refl

⊢ ∀x. max x x = x

max_le2_imp

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

max_le

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

max_infty

⊢ ∀x.
      (max x PosInf = PosInf) ∧ (max PosInf x = PosInf) ∧ (max NegInf x = x) ∧
      (max x NegInf = x)

max_comm

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

lte_trans

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

lte_mul

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

lte_add

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

lt_trans

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

lt_total

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

lt_sub_imp

⊢ ∀x y z. y + x < z ⇒ y < z − x

lt_sub

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

lt_rmul

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

lt_refl

⊢ ∀x. ¬(x < x)

lt_rdiv_neg

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

lt_rdiv

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

lt_radd

⊢ ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y + x < z + x ⇔ y < z)

lt_neg

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

lt_mul_neg

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

lt_mul2

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

lt_mul

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

lt_lmul

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

lt_le

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

lt_ldiv

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

lt_ladd

⊢ ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x + y < x + z ⇔ y < z)

lt_infty

⊢ ∀x y.
      NegInf < Normal y ∧ Normal y < PosInf ∧ NegInf < PosInf ∧
      ¬(x < NegInf) ∧ ¬(PosInf < x) ∧ (x ≠ PosInf ⇔ x < PosInf) ∧
      (x ≠ NegInf ⇔ NegInf < x)

lt_imp_ne

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

lt_imp_le

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

lt_antisym

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

lt_addl

⊢ ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (y < x + y ⇔ 0 < x)

lt_add2

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

lt_add

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

lt_02

⊢ 0 < 2

lt_01

⊢ 0 < 1

logr_not_infty

⊢ ∀x b. x ≠ NegInf ∧ x ≠ PosInf ⇒ logr b x ≠ NegInf ∧ logr b x ≠ PosInf

LOGR_MONO_LE_IMP

⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y

LOGR_MONO_LE

⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)

linv_uniq

⊢ ∀x y. (x * y = 1) ⇒ (x = inv y)

let_trans

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

let_mul

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

let_add2_alt

⊢ ∀w x y z. x ≠ NegInf ∧ x ≠ PosInf ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

let_add2

⊢ ∀w x y z. w ≠ NegInf ∧ w ≠ PosInf ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

let_add

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

le_trans

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

le_total

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

le_sup_imp

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

le_sup

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

le_sub_imp

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

le_sub_eq2

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

le_sub_eq

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

le_rmul_imp

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

le_refl

⊢ ∀x. x ≤ x

le_rdiv

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

le_radd_imp

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

le_radd

⊢ ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y + x ≤ z + x ⇔ y ≤ z)

le_pow2

⊢ ∀x. 0 ≤ x pow 2

le_num

⊢ ∀n. 0 ≤ &n

le_neg

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

le_mul_neg

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

le_mul_epsilon

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

le_mul

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

le_min

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

le_max2

⊢ ∀x y. y ≤ max x y

le_max1

⊢ ∀x y. x ≤ max x y

le_max

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

le_lt

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

le_lsub_imp

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

le_lneg

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

le_lmul_imp

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

le_ldiv

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

le_ladd_imp

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

le_ladd

⊢ ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x + y ≤ x + z ⇔ y ≤ z)

le_inv

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ inv x

le_infty

⊢ (∀x. NegInf ≤ x ∧ x ≤ PosInf) ∧ (∀x. x ≤ NegInf ⇔ (x = NegInf)) ∧
  ∀x. PosInf ≤ x ⇔ (x = PosInf)

le_inf

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

le_epsilon

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

le_antisym

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

le_addr_imp

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

le_addr

⊢ ∀x y. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x ≤ x + y ⇔ 0 ≤ y)

le_add2

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

le_add

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

le_02

⊢ 0 ≤ 2

le_01

⊢ 0 ≤ 1

inv_pos

⊢ ∀x. 0 < x ∧ x ≠ PosInf ⇒ 0 < 1 / x

inv_one

⊢ inv 1 = 1

INV_IN_Q

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

inv_1over

⊢ ∀x. inv x = 1 / x

inf_suc

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

inf_seq

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

inf_min

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

inf_lt_infty

⊢ ∀p. NegInf < inf p ⇒ ∀x. p x ⇒ NegInf < x

inf_le_imp

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

inf_le

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

inf_eq

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

inf_const_over_set

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

inf_const_alt

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

inf_const

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

inf_cminus

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

half_cancel

⊢ 2 * (1 / 2) = 1

half_between

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

fourth_cancel

⊢ 4 * (1 / 4) = 1

EXTREAL_SUM_IMAGE_ZERO_DIFF

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

EXTREAL_SUM_IMAGE_ZERO

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

EXTREAL_SUM_IMAGE_THM

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

EXTREAL_SUM_IMAGE_SUB

⊢ ∀s.
      FINITE s ⇒
      ∀f f'.
          (∀x. x ∈ s ⇒ f' x ≠ NegInf) ∨ (∀x. x ∈ s ⇒ f' x ≠ PosInf) ⇒
          (SIGMA (λx. f x − f' x) s = SIGMA f s − SIGMA f' s)

EXTREAL_SUM_IMAGE_SPOS

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

EXTREAL_SUM_IMAGE_SING

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

EXTREAL_SUM_IMAGE_POS_MEM_LE

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

EXTREAL_SUM_IMAGE_POS

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

EXTREAL_SUM_IMAGE_NOT_POS_INF

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ PosInf) ⇒ SIGMA f s ≠ PosInf

EXTREAL_SUM_IMAGE_NOT_NEG_INF

⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒ SIGMA f s ≠ NegInf

EXTREAL_SUM_IMAGE_NOT_INFTY

⊢ ∀f s.
      (FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒ SIGMA f s ≠ NegInf) ∧
      (FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ PosInf) ⇒ SIGMA f s ≠ PosInf)

EXTREAL_SUM_IMAGE_NORMAL

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

EXTREAL_SUM_IMAGE_MONO_SET

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

EXTREAL_SUM_IMAGE_MONO

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

EXTREAL_SUM_IMAGE_INV_CARD_EQ_1

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

EXTREAL_SUM_IMAGE_INTER_NONZERO

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

EXTREAL_SUM_IMAGE_INTER_ELIM

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

EXTREAL_SUM_IMAGE_IN_IF_ALT

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

EXTREAL_SUM_IMAGE_IN_IF

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

EXTREAL_SUM_IMAGE_IMAGE

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

EXTREAL_SUM_IMAGE_IF_ELIM

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

EXTREAL_SUM_IMAGE_FINITE_SAME

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

EXTREAL_SUM_IMAGE_FINITE_CONST

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

EXTREAL_SUM_IMAGE_EXTREAL_SUM_IMAGE

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

EXTREAL_SUM_IMAGE_EQ_CARD

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

EXTREAL_SUM_IMAGE_EQ

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

EXTREAL_SUM_IMAGE_DISJOINT_UNION

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

EXTREAL_SUM_IMAGE_CROSS_SYM

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

EXTREAL_SUM_IMAGE_COUNT

⊢ ∀f.
      (SIGMA f (count 2) = f 0 + f 1) ∧
      (SIGMA f (count 3) = f 0 + f 1 + f 2) ∧
      (SIGMA f (count 4) = f 0 + f 1 + f 2 + f 3) ∧
      (SIGMA f (count 5) = f 0 + f 1 + f 2 + f 3 + f 4)

EXTREAL_SUM_IMAGE_CMUL2

⊢ ∀s f c.
      FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒
      (SIGMA (λx. Normal c * f x) s = Normal c * SIGMA f s)

EXTREAL_SUM_IMAGE_CMUL

⊢ ∀s.
      FINITE s ⇒
      ∀f c.
          0 ≤ c ∨ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒
          (SIGMA (λx. Normal c * f x) s = Normal c * SIGMA f s)

EXTREAL_SUM_IMAGE_ADD

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

EXTREAL_SUM_IMAGE_0

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

extreal_sub_ind

⊢ ∀P.
      (∀x y. P (Normal x) (Normal y)) ∧ (∀a. P PosInf a) ∧ P NegInf PosInf ∧
      (∀v2. P (Normal v2) PosInf) ∧ P NegInf NegInf ∧
      (∀v5. P NegInf (Normal v5)) ∧ (∀v3. P (Normal v3) NegInf) ⇒
      ∀v v1. P v v1

extreal_sub_def

⊢ (Normal x − Normal y = Normal (x − y)) ∧ (PosInf − a = PosInf) ∧
  (NegInf − PosInf = NegInf) ∧ (Normal v2 − PosInf = NegInf) ∧
  (NegInf − NegInf = PosInf) ∧ (NegInf − Normal v5 = NegInf) ∧
  (Normal v3 − NegInf = PosInf)

extreal_sub_add

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

extreal_not_infty

⊢ ∀x. Normal x ≠ NegInf ∧ Normal x ≠ PosInf

extreal_nchotomy

⊢ ∀ee. (ee = NegInf) ∨ (ee = PosInf) ∨ ∃r. ee = Normal r

extreal_mul_ind

⊢ ∀P.
      P NegInf NegInf ∧ P NegInf PosInf ∧ P PosInf NegInf ∧ P PosInf PosInf ∧
      (∀x. P (Normal x) NegInf) ∧ (∀y. P NegInf (Normal y)) ∧
      (∀x. P (Normal x) PosInf) ∧ (∀y. P PosInf (Normal y)) ∧
      (∀x y. P (Normal x) (Normal y)) ⇒
      ∀v v1. P v v1

extreal_mul_def

⊢ (NegInf * NegInf = PosInf) ∧ (NegInf * PosInf = NegInf) ∧
  (PosInf * NegInf = NegInf) ∧ (PosInf * PosInf = PosInf) ∧
  (Normal x * NegInf =
   if x = 0 then Normal 0 else if 0 < x then NegInf else PosInf) ∧
  (NegInf * Normal y =
   if y = 0 then Normal 0 else if 0 < y then NegInf else PosInf) ∧
  (Normal x * PosInf =
   if x = 0 then Normal 0 else if 0 < x then PosInf else NegInf) ∧
  (PosInf * Normal y =
   if y = 0 then Normal 0 else if 0 < y then PosInf else NegInf) ∧
  (Normal x * Normal y = Normal (x * y))

extreal_lt_eq

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

extreal_le_ind

⊢ ∀P.
      (∀x y. P (Normal x) (Normal y)) ∧ (∀a. P NegInf a) ∧ P PosInf PosInf ∧
      (∀v2. P (Normal v2) PosInf) ∧ P PosInf NegInf ∧
      (∀v3. P (Normal v3) NegInf) ∧ (∀v5. P PosInf (Normal v5)) ⇒
      ∀v v1. P v v1

extreal_le_def

⊢ (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (NegInf ≤ a ⇔ T) ∧ (PosInf ≤ PosInf ⇔ T) ∧
  (Normal v2 ≤ PosInf ⇔ T) ∧ (PosInf ≤ NegInf ⇔ F) ∧
  (Normal v3 ≤ NegInf ⇔ F) ∧ (PosInf ≤ Normal v5 ⇔ F)

extreal_induction

⊢ ∀P. P NegInf ∧ P PosInf ∧ (∀r. P (Normal r)) ⇒ ∀e. P e

extreal_eq_zero

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

EXTREAL_EQ_LADD

⊢ ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ ((x + y = x + z) ⇔ (y = z))

extreal_div_eq

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

extreal_distinct

⊢ NegInf ≠ PosInf ∧ (∀a. NegInf ≠ Normal a) ∧ ∀a. PosInf ≠ Normal a

extreal_cases

⊢ ∀x. (x = NegInf) ∨ (x = PosInf) ∨ ∃r. x = Normal r

extreal_case_eq

⊢ (extreal_CASE x v v1 f = v') ⇔
  (x = NegInf) ∧ (v = v') ∨ (x = PosInf) ∧ (v1 = v') ∨
  ∃r. (x = Normal r) ∧ (f r = v')

extreal_case_cong

⊢ ∀M M' v v1 f.
      (M = M') ∧ ((M' = NegInf) ⇒ (v = v')) ∧ ((M' = PosInf) ⇒ (v1 = v1')) ∧
      (∀a. (M' = Normal a) ⇒ (f a = f' a)) ⇒
      (extreal_CASE M v v1 f = extreal_CASE M' v' v1' f')

extreal_Axiom

⊢ ∀f0 f1 f2.
      ∃fn. (fn NegInf = f0) ∧ (fn PosInf = f1) ∧ ∀a. fn (Normal a) = f2 a

EXTREAL_ARCH_POW_INV

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

EXTREAL_ARCH_POW

⊢ ∀x. x ≠ PosInf ⇒ ∃n. x < 2 pow n

EXTREAL_ARCH

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

extreal_add_ind

⊢ ∀P.
      (∀x y. P (Normal x) (Normal y)) ∧ (∀a. P PosInf a) ∧ P NegInf PosInf ∧
      (∀v2. P (Normal v2) PosInf) ∧ P NegInf NegInf ∧
      (∀v5. P NegInf (Normal v5)) ∧ (∀v3. P (Normal v3) NegInf) ⇒
      ∀v v1. P v v1

extreal_add_def

⊢ (Normal x + Normal y = Normal (x + y)) ∧ (PosInf + a = PosInf) ∧
  (NegInf + PosInf = PosInf) ∧ (Normal v2 + PosInf = PosInf) ∧
  (NegInf + NegInf = NegInf) ∧ (NegInf + Normal v5 = NegInf) ∧
  (Normal v3 + NegInf = NegInf)

extreal_abs_ind

⊢ ∀P. (∀x. P (Normal x)) ∧ P NegInf ∧ P PosInf ⇒ ∀v. P v

extreal_abs_def

⊢ (abs (Normal x) = Normal (abs x)) ∧ (abs NegInf = PosInf) ∧
  (abs PosInf = PosInf)

extreal_11

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

ext_suminf_suminf

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

ext_suminf_sum

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

ext_suminf_sub

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

ext_suminf_mono

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

ext_suminf_lt_infty

⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f ≠ PosInf ⇒ ∀n. f n < PosInf

ext_suminf_cmul_alt

⊢ ∀f c.
      0 ≤ c ∧ ((∀n. f n ≠ NegInf) ∨ ∀n. f n ≠ PosInf) ⇒
      (suminf (λn. Normal c * f n) = Normal c * suminf f)

ext_suminf_cmul

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

ext_suminf_add

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

ext_mono_increasing_suc

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

ext_mono_decreasing_suc

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

eq_sub_switch

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

eq_sub_radd

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

eq_sub_ladd_normal

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

eq_sub_ladd

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

eq_neg

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

eq_add_sub_switch

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

entire

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

div_one

⊢ ∀x. x / 1 = x

DIV_IN_Q

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

div_add

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

datatype_extreal

⊢ DATATYPE (extreal NegInf PosInf Normal)

CROSS_COUNTABLE_UNIV

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

CROSS_COUNTABLE_LEMMA2

⊢ ∀s. COUNTABLE s ∧ COUNTABLE t ∧ FINITE t ⇒ COUNTABLE (s × t)

CROSS_COUNTABLE_LEMMA1

⊢ ∀s. COUNTABLE s ∧ FINITE s ∧ COUNTABLE t ⇒ COUNTABLE (s × t)

CROSS_COUNTABLE

⊢ ∀s. COUNTABLE s ∧ COUNTABLE t ⇒ COUNTABLE (s × t)

COUNTABLE_RATIONAL_INTERVALS

⊢ COUNTABLE rational_intervals

COUNTABLE_ENUM_Q

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

CMUL_IN_Q

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

CEILING_UBOUND

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

CEILING_LBOUND

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

add_sub2

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

add_sub

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

add_rzero

⊢ ∀x. x + 0 = x

add_rdistrib_normal2

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

add_rdistrib_normal

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

add_rdistrib

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

add_pow2

⊢ ∀x y. (x + y) pow 2 = x pow 2 + y pow 2 + 2 * x * y

add_not_infty

⊢ ∀x y.
      (x ≠ NegInf ∧ y ≠ NegInf ⇒ x + y ≠ NegInf) ∧
      (x ≠ PosInf ∧ y ≠ PosInf ⇒ x + y ≠ PosInf)

add_lzero

⊢ ∀x. 0 + x = x

add_ldistrib_pos

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

add_ldistrib_normal2

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

add_ldistrib_normal

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

add_ldistrib_neg

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

add_ldistrib

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

add_infty

⊢ (∀x. (x + PosInf = PosInf) ∧ (PosInf + x = PosInf)) ∧
  ∀x. x ≠ PosInf ⇒ (x + NegInf = NegInf) ∧ (NegInf + x = NegInf)

ADD_IN_Q

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

add_comm

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

add_assoc

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

add2_sub2

⊢ ∀a b c d.
      b ≠ PosInf ∧ d ≠ PosInf ∨ b ≠ NegInf ∧ d ≠ NegInf ⇒
      (a − b + (c − d) = a + c − (b + d))

abs_refl

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

abs_pos

⊢ ∀x. 0 ≤ abs x

abs_bounds_lt

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

abs_bounds

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