Structure extrealTheory


Source File Identifier index Theory binding index

signature extrealTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val EXTREAL_PROD_IMAGE_DEF : thm
    val EXTREAL_SUM_IMAGE_DEF : thm
    val Q_set_def : thm
    val ceiling_def : thm
    val ext_liminf_def : thm
    val ext_limsup_def : thm
    val ext_mono_decreasing_def : thm
    val ext_mono_increasing_def : thm
    val ext_suminf_def : thm
    val extreal_TY_DEF : thm
    val extreal_abs_primitive_def : thm
    val extreal_ainv_def : thm
    val extreal_case_def : thm
    val extreal_div_def : thm
    val extreal_exp_def : thm
    val extreal_inf_def : thm
    val extreal_inv_def : thm
    val extreal_lg_def : thm
    val extreal_ln_def : thm
    val extreal_logr_def : thm
    val extreal_lt_def : thm
    val extreal_max_def : thm
    val extreal_min_def : thm
    val extreal_of_num_def : thm
    val extreal_pow_def : thm
    val extreal_powr_def : thm
    val extreal_size_def : thm
    val extreal_sqrt_def : thm
    val extreal_sup_def : thm
    val max_fn_seq_def : thm
    val open_interval_def : thm
    val open_intervals_def : thm
    val rational_intervals_def : thm
    val real_def : thm
    val real_set_def : thm
    val seq_sup_def : thm
  
  (*  Theorems  *)
    val ABS_LE_HALF_POW2 : thm
    val ADD_IN_Q : thm
    val CEILING_LBOUND : thm
    val CEILING_UBOUND : thm
    val CMUL_IN_Q : thm
    val COUNTABLE_ENUM_Q : thm
    val COUNTABLE_RATIONAL_INTERVALS : thm
    val CROSS_COUNTABLE_UNIV : thm
    val DIV_IN_Q : thm
    val EXTREAL_ARCH : thm
    val EXTREAL_ARCH_POW : thm
    val EXTREAL_ARCH_POW_INV : thm
    val EXTREAL_EQ_LADD : thm
    val EXTREAL_EQ_RADD : thm
    val EXTREAL_PROD_IMAGE_DISJOINT_UNION : thm
    val EXTREAL_PROD_IMAGE_EMPTY : thm
    val EXTREAL_PROD_IMAGE_EQ : thm
    val EXTREAL_PROD_IMAGE_IMAGE : thm
    val EXTREAL_PROD_IMAGE_PAIR : thm
    val EXTREAL_PROD_IMAGE_PROPERTY : thm
    val EXTREAL_PROD_IMAGE_SING : thm
    val EXTREAL_PROD_IMAGE_THM : thm
    val EXTREAL_SUM_IMAGE_0 : thm
    val EXTREAL_SUM_IMAGE_ADD : thm
    val EXTREAL_SUM_IMAGE_CMUL : thm
    val EXTREAL_SUM_IMAGE_COUNT : thm
    val EXTREAL_SUM_IMAGE_DISJOINT_UNION : thm
    val EXTREAL_SUM_IMAGE_EMPTY : thm
    val EXTREAL_SUM_IMAGE_EQ : thm
    val EXTREAL_SUM_IMAGE_EQ_CARD : thm
    val EXTREAL_SUM_IMAGE_FINITE_CONST : thm
    val EXTREAL_SUM_IMAGE_FINITE_SAME : thm
    val EXTREAL_SUM_IMAGE_IF_ELIM : thm
    val EXTREAL_SUM_IMAGE_IMAGE : thm
    val EXTREAL_SUM_IMAGE_INSERT : thm
    val EXTREAL_SUM_IMAGE_INTER_ELIM : thm
    val EXTREAL_SUM_IMAGE_INTER_NONZERO : thm
    val EXTREAL_SUM_IMAGE_INV_CARD_EQ_1 : thm
    val EXTREAL_SUM_IMAGE_IN_IF : thm
    val EXTREAL_SUM_IMAGE_IN_IF_ALT : thm
    val EXTREAL_SUM_IMAGE_MONO : thm
    val EXTREAL_SUM_IMAGE_MONO_SET : thm
    val EXTREAL_SUM_IMAGE_NEG : thm
    val EXTREAL_SUM_IMAGE_NORMAL : thm
    val EXTREAL_SUM_IMAGE_NOT_INFTY : thm
    val EXTREAL_SUM_IMAGE_NOT_NEGINF : thm
    val EXTREAL_SUM_IMAGE_NOT_POSINF : thm
    val EXTREAL_SUM_IMAGE_PERMUTES : thm
    val EXTREAL_SUM_IMAGE_POS : thm
    val EXTREAL_SUM_IMAGE_POS_MEM_LE : thm
    val EXTREAL_SUM_IMAGE_POW : thm
    val EXTREAL_SUM_IMAGE_PROPERTY : thm
    val EXTREAL_SUM_IMAGE_PROPERTY_NEG : thm
    val EXTREAL_SUM_IMAGE_PROPERTY_POS : thm
    val EXTREAL_SUM_IMAGE_SING : thm
    val EXTREAL_SUM_IMAGE_SNEG : thm
    val EXTREAL_SUM_IMAGE_SPOS : thm
    val EXTREAL_SUM_IMAGE_SUB : thm
    val EXTREAL_SUM_IMAGE_SUM_IMAGE : thm
    val EXTREAL_SUM_IMAGE_SUM_IMAGE_MONO : thm
    val EXTREAL_SUM_IMAGE_THM : thm
    val EXTREAL_SUM_IMAGE_ZERO : thm
    val EXTREAL_SUM_IMAGE_ZERO_DIFF : thm
    val EXTREAL_SUM_IMAGE_le_suminf : thm
    val EXTREAL_SUP_FUN_SEQ_IMAGE : thm
    val EXTREAL_SUP_FUN_SEQ_MONO_IMAGE : thm
    val EXTREAL_SUP_SEQ : thm
    val INV_IN_Q : thm
    val MUL_IN_Q : thm
    val NESTED_EXTREAL_SUM_IMAGE_REVERSE : thm
    val NUM_IN_Q : thm
    val OPP_IN_Q : thm
    val Q_COUNTABLE : thm
    val Q_DENSE_IN_R : thm
    val Q_DENSE_IN_R_LEMMA : thm
    val Q_INFINITE : thm
    val Q_not_infty : thm
    val REAL_LE_MUL_EPSILON : thm
    val REAL_LE_RSUB_GE0 : thm
    val SIMP_EXTREAL_ARCH : thm
    val SIMP_EXTREAL_ARCH_NEG : thm
    val SUB_IN_Q : thm
    val abs_0 : thm
    val abs_abs : thm
    val abs_bounds : thm
    val abs_bounds_lt : thm
    val abs_div : thm
    val abs_eq_0 : thm
    val abs_gt_0 : thm
    val abs_le_0 : thm
    val abs_le_half_pow2 : thm
    val abs_le_square_plus1 : thm
    val abs_max : thm
    val abs_mul : thm
    val abs_neg : thm
    val abs_not_infty : thm
    val abs_pos : thm
    val abs_pow2 : thm
    val abs_pow_le_mono : thm
    val abs_refl : thm
    val abs_triangle : thm
    val abs_triangle_sub : thm
    val abs_unbounds : thm
    val add2_sub2 : thm
    val add_assoc : thm
    val add_comm : thm
    val add_comm_normal : thm
    val add_infty : thm
    val add_ldistrib : thm
    val add_ldistrib_neg : thm
    val add_ldistrib_normal : thm
    val add_ldistrib_normal2 : thm
    val add_ldistrib_pos : thm
    val add_lzero : thm
    val add_not_infty : thm
    val add_pow2 : thm
    val add_pow2_pos : thm
    val add_rdistrib : thm
    val add_rdistrib_normal : thm
    val add_rdistrib_normal2 : thm
    val add_rzero : thm
    val add_sub : thm
    val add_sub2 : thm
    val datatype_extreal : thm
    val div_add : thm
    val div_add2 : thm
    val div_eq_mul_linv : thm
    val div_infty : thm
    val div_mul_refl : thm
    val div_not_infty : thm
    val div_one : thm
    val div_refl : thm
    val div_refl_pos : thm
    val entire : thm
    val eq_add_sub_switch : thm
    val eq_neg : thm
    val eq_sub_ladd : thm
    val eq_sub_ladd_normal : thm
    val eq_sub_radd : thm
    val eq_sub_switch : thm
    val exp_0 : thm
    val exp_pos : thm
    val ext_mono_decreasing_suc : thm
    val ext_mono_increasing_suc : thm
    val ext_suminf_0 : thm
    val ext_suminf_2d : thm
    val ext_suminf_2d_full : thm
    val ext_suminf_add : thm
    val ext_suminf_alt : thm
    val ext_suminf_alt' : thm
    val ext_suminf_cmul : thm
    val ext_suminf_cmul_alt : thm
    val ext_suminf_eq : thm
    val ext_suminf_eq_infty : thm
    val ext_suminf_eq_infty_imp : thm
    val ext_suminf_lt_infty : thm
    val ext_suminf_mono : thm
    val ext_suminf_pos : thm
    val ext_suminf_posinf : thm
    val ext_suminf_real_suminf : thm
    val ext_suminf_sigma : thm
    val ext_suminf_sigma' : thm
    val ext_suminf_sing : thm
    val ext_suminf_sub : thm
    val ext_suminf_sum : thm
    val ext_suminf_suminf : thm
    val ext_suminf_suminf' : thm
    val ext_suminf_summable : thm
    val ext_suminf_sup_eq : thm
    val ext_suminf_zero : thm
    val extreal_11 : thm
    val extreal_Axiom : thm
    val extreal_abs_def : thm
    val extreal_abs_ind : thm
    val extreal_add_def : thm
    val extreal_add_eq : thm
    val extreal_add_ind : thm
    val extreal_case_cong : thm
    val extreal_case_eq : thm
    val extreal_cases : thm
    val extreal_distinct : thm
    val extreal_div_eq : thm
    val extreal_eq_zero : thm
    val extreal_induction : thm
    val extreal_inv_eq : thm
    val extreal_le_def : thm
    val extreal_le_eq : thm
    val extreal_le_ind : thm
    val extreal_lt_eq : thm
    val extreal_mean : thm
    val extreal_mul_def : thm
    val extreal_mul_ind : thm
    val extreal_nchotomy : thm
    val extreal_not_infty : thm
    val extreal_not_lt : thm
    val extreal_sub_add : thm
    val extreal_sub_def : thm
    val extreal_sub_eq : thm
    val extreal_sub_ind : thm
    val fourth_cancel : thm
    val fourths_between : thm
    val gen_powr : thm
    val half_between : thm
    val half_cancel : thm
    val half_not_infty : thm
    val harmonic_series_pow_2 : thm
    val inf_cminus : thm
    val inf_const : thm
    val inf_const_alt : thm
    val inf_const_over_set : thm
    val inf_empty : thm
    val inf_eq : thm
    val inf_eq' : thm
    val inf_le : thm
    val inf_le' : thm
    val inf_le_imp : thm
    val inf_le_imp' : thm
    val inf_lt : thm
    val inf_lt' : thm
    val inf_lt_infty : thm
    val inf_min : thm
    val inf_minimal : thm
    val inf_mono_subset : thm
    val inf_seq : thm
    val inf_sing : thm
    val inf_suc : thm
    val inf_univ : thm
    val infty_div : thm
    val inv_1over : thm
    val inv_inj : thm
    val inv_le_antimono : thm
    val inv_lt_antimono : thm
    val inv_mul : thm
    val inv_not_infty : thm
    val inv_one : thm
    val inv_pos : thm
    val inv_pos' : thm
    val inv_pos_eq : thm
    val ldiv_eq : thm
    val ldiv_le_imp : thm
    val le_01 : thm
    val le_02 : thm
    val le_abs : thm
    val le_abs_bounds : thm
    val le_add : thm
    val le_add2 : thm
    val le_add_neg : thm
    val le_addl_imp : thm
    val le_addr : thm
    val le_addr_imp : thm
    val le_antisym : thm
    val le_div : thm
    val le_epsilon : thm
    val le_inf : thm
    val le_inf' : thm
    val le_inf_epsilon_set : thm
    val le_infty : thm
    val le_inv : thm
    val le_ladd : thm
    val le_ladd_imp : thm
    val le_ldiv : thm
    val le_lmul_imp : thm
    val le_lneg : thm
    val le_lsub_imp : thm
    val le_lt : thm
    val le_max : thm
    val le_max1 : thm
    val le_max2 : thm
    val le_min : thm
    val le_mul : thm
    val le_mul_epsilon : thm
    val le_mul_neg : thm
    val le_neg : thm
    val le_not_infty : thm
    val le_num : thm
    val le_pow2 : thm
    val le_radd : thm
    val le_radd_imp : thm
    val le_rdiv : thm
    val le_refl : thm
    val le_rmul_imp : thm
    val le_rsub_imp : thm
    val le_sub_eq : thm
    val le_sub_eq2 : thm
    val le_sub_imp : thm
    val le_sub_imp2 : thm
    val le_sup : thm
    val le_sup' : thm
    val le_sup_imp : thm
    val le_sup_imp' : thm
    val le_sup_imp2 : thm
    val le_total : thm
    val le_trans : thm
    val let_add : thm
    val let_add2 : thm
    val let_add2_alt : thm
    val let_antisym : thm
    val let_mul : thm
    val let_total : thm
    val let_trans : thm
    val linv_uniq : thm
    val logr_not_infty : thm
    val lt_01 : thm
    val lt_02 : thm
    val lt_10 : thm
    val lt_abs_bounds : thm
    val lt_add : thm
    val lt_add2 : thm
    val lt_add_neg : thm
    val lt_addl : thm
    val lt_addr_imp : thm
    val lt_antisym : thm
    val lt_div : thm
    val lt_imp_le : thm
    val lt_imp_ne : thm
    val lt_inf_epsilon : thm
    val lt_inf_epsilon_set : thm
    val lt_infty : thm
    val lt_ladd : thm
    val lt_ldiv : thm
    val lt_le : thm
    val lt_lmul : thm
    val lt_max_between : thm
    val lt_mul : thm
    val lt_mul2 : thm
    val lt_mul_neg : thm
    val lt_neg : thm
    val lt_radd : thm
    val lt_rdiv : thm
    val lt_rdiv_neg : thm
    val lt_refl : thm
    val lt_rmul : thm
    val lt_sub : thm
    val lt_sub' : thm
    val lt_sub_imp : thm
    val lt_sub_imp' : thm
    val lt_sub_imp2 : thm
    val lt_sup : thm
    val lt_total : thm
    val lt_trans : thm
    val lte_add : thm
    val lte_mul : thm
    val lte_total : thm
    val lte_trans : thm
    val max_comm : thm
    val max_fn_seq_compute : thm
    val max_fn_seq_mono : thm
    val max_infty : thm
    val max_le : thm
    val max_le2_imp : thm
    val max_reduce : thm
    val max_refl : thm
    val min_comm : thm
    val min_infty : thm
    val min_le : thm
    val min_le1 : thm
    val min_le2 : thm
    val min_le2_imp : thm
    val min_le_between : thm
    val min_reduce : thm
    val min_refl : thm
    val mul_assoc : thm
    val mul_comm : thm
    val mul_div_refl : thm
    val mul_infty : thm
    val mul_lcancel : thm
    val mul_le : thm
    val mul_le2 : thm
    val mul_let : thm
    val mul_linv : thm
    val mul_linv_pos : thm
    val mul_lneg : thm
    val mul_lone : thm
    val mul_lposinf : thm
    val mul_lt : thm
    val mul_lt2 : thm
    val mul_lte : thm
    val mul_lzero : thm
    val mul_not_infty : thm
    val mul_not_infty2 : thm
    val mul_rneg : thm
    val mul_rone : thm
    val mul_rposinf : thm
    val mul_rzero : thm
    val ne_01 : thm
    val ne_02 : thm
    val neg_0 : thm
    val neg_add : thm
    val neg_eq0 : thm
    val neg_minus1 : thm
    val neg_mul2 : thm
    val neg_neg : thm
    val neg_not_posinf : thm
    val neg_sub : thm
    val normal_exp : thm
    val normal_inv_eq : thm
    val normal_powr : thm
    val normal_real : thm
    val normal_real_set : thm
    val num_lt_infty : thm
    val num_not_infty : thm
    val one_pow : thm
    val pos_not_neginf : thm
    val pos_summable : thm
    val pow2_le_eq : thm
    val pow2_sqrt : thm
    val pow_0 : thm
    val pow_1 : thm
    val pow_2 : thm
    val pow_add : thm
    val pow_div : thm
    val pow_half_pos_le : thm
    val pow_half_pos_lt : thm
    val pow_half_ser : thm
    val pow_half_ser' : thm
    val pow_half_ser_by_e : thm
    val pow_inv : thm
    val pow_le : thm
    val pow_le_full : thm
    val pow_le_mono : thm
    val pow_lt : thm
    val pow_lt2 : thm
    val pow_minus1 : thm
    val pow_mul : thm
    val pow_neg_odd : thm
    val pow_not_infty : thm
    val pow_pos_even : thm
    val pow_pos_le : thm
    val pow_pos_lt : thm
    val pow_zero : thm
    val pow_zero_imp : thm
    val powr_0 : thm
    val powr_pos : thm
    val quotient_normal : thm
    val rat_not_infty : thm
    val rdiv_eq : thm
    val real_normal : thm
    val rinv_uniq : thm
    val seq_sup_compute : thm
    val sqrt_mono_le : thm
    val sqrt_pos_le : thm
    val sqrt_pos_lt : thm
    val sqrt_pow2 : thm
    val sub_0 : thm
    val sub_add : thm
    val sub_add2 : thm
    val sub_eq_0 : thm
    val sub_infty : thm
    val sub_ldistrib : thm
    val sub_le_eq : thm
    val sub_le_eq2 : thm
    val sub_le_imp : thm
    val sub_le_imp2 : thm
    val sub_le_switch : thm
    val sub_le_switch2 : thm
    val sub_le_zero : thm
    val sub_lneg : thm
    val sub_lt_eq : thm
    val sub_lt_imp : thm
    val sub_lt_imp2 : thm
    val sub_lt_zero : thm
    val sub_lt_zero2 : thm
    val sub_lzero : thm
    val sub_not_infty : thm
    val sub_pow2 : thm
    val sub_rdistrib : thm
    val sub_refl : thm
    val sub_rneg : thm
    val sub_rzero : thm
    val sub_zero_le : thm
    val sub_zero_lt : thm
    val sub_zero_lt2 : thm
    val summable_ext_suminf : thm
    val summable_ext_suminf_suminf : thm
    val sup_add_mono : thm
    val sup_close : thm
    val sup_cmul : thm
    val sup_cmult : thm
    val sup_comm : thm
    val sup_const : thm
    val sup_const_alt : thm
    val sup_const_alt' : thm
    val sup_const_over_set : thm
    val sup_const_over_univ : thm
    val sup_countable_seq : thm
    val sup_empty : thm
    val sup_eq : thm
    val sup_eq' : thm
    val sup_le : thm
    val sup_le' : thm
    val sup_le_mono : thm
    val sup_le_sup_imp : thm
    val sup_le_sup_imp' : thm
    val sup_lt : thm
    val sup_lt' : thm
    val sup_lt_epsilon : thm
    val sup_lt_infty : thm
    val sup_max : thm
    val sup_maximal : thm
    val sup_mono : thm
    val sup_mono_ext : thm
    val sup_mono_subset : thm
    val sup_num : thm
    val sup_seq : thm
    val sup_seq_countable_seq : thm
    val sup_shift : thm
    val sup_sing : thm
    val sup_suc : thm
    val sup_sum_mono : thm
    val sup_univ : thm
    val third_cancel : thm
    val thirds_between : thm
    val zero_div : thm
    val zero_pow : thm
    val zero_rpow : thm
  
  val extreal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [cardinal] Parent theory of "extreal"
   
   [util_prob] Parent theory of "extreal"
   
   [EXTREAL_PROD_IMAGE_DEF]  Definition
      
      ⊢ ∀f s. ∏ f s = ITSET (λe acc. f e * acc) s 1
   
   [EXTREAL_SUM_IMAGE_DEF]  Definition
      
      ⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0
   
   [Q_set_def]  Definition
      
      ⊢ ℚ =
        {x | ∃a b. x = &a / &b ∧ 0 < &b} ∪
        {x | ∃a b. x = -(&a / &b) ∧ 0 < &b}
   
   [ceiling_def]  Definition
      
      ⊢ ∀x. ceiling (Normal x) = LEAST n. x ≤ &n
   
   [ext_liminf_def]  Definition
      
      ⊢ ∀a. liminf a = sup (IMAGE (λm. inf {a n | m ≤ n}) 𝕌(:num))
   
   [ext_limsup_def]  Definition
      
      ⊢ ∀a. limsup a = inf (IMAGE (λm. sup {a n | m ≤ n}) 𝕌(:num))
   
   [ext_mono_decreasing_def]  Definition
      
      ⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m
   
   [ext_mono_increasing_def]  Definition
      
      ⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n
   
   [ext_suminf_def]  Definition
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ⇒
            suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))
   
   [extreal_TY_DEF]  Definition
      
      ⊢ ∃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]  Definition
      
      ⊢ abs =
        WFREC (@R. WF R)
          (λextreal_abs a.
               case a of
                 −∞ => I +∞
               | +∞ => I +∞
               | Normal x => I (Normal (abs x)))
   
   [extreal_ainv_def]  Definition
      
      ⊢ -−∞ = +∞ ∧ -+∞ = −∞ ∧ ∀x. -Normal x = Normal (-x)
   
   [extreal_case_def]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ (∀r. Normal r / +∞ = Normal 0) ∧ (∀r. Normal r / −∞ = Normal 0) ∧
        ∀x r. r ≠ 0 ⇒ x / Normal r = x * (Normal r)⁻¹
   
   [extreal_exp_def]  Definition
      
      ⊢ (∀x. exp (Normal x) = Normal (exp x)) ∧ exp +∞ = +∞ ∧
        exp −∞ = Normal 0
   
   [extreal_inf_def]  Definition
      
      ⊢ ∀p. inf p = -sup (IMAGE numeric_negate p)
   
   [extreal_inv_def]  Definition
      
      ⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
        ∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹
   
   [extreal_lg_def]  Definition
      
      ⊢ ∀x. lg x = logr 2 x
   
   [extreal_ln_def]  Definition
      
      ⊢ (∀x. 0 < x ⇒ ln (Normal x) = Normal (ln x)) ∧ ln (Normal 0) = −∞ ∧
        ln +∞ = +∞
   
   [extreal_logr_def]  Definition
      
      ⊢ (∀b x. logr b (Normal x) = Normal (logr b x)) ∧ ∀b. logr b +∞ = +∞
   
   [extreal_lt_def]  Definition
      
      ⊢ ∀x y. x < y ⇔ ¬(y ≤ x)
   
   [extreal_max_def]  Definition
      
      ⊢ ∀x y. max x y = if x ≤ y then y else x
   
   [extreal_min_def]  Definition
      
      ⊢ ∀x y. min x y = if x ≤ y then x else y
   
   [extreal_of_num_def]  Definition
      
      ⊢ ∀n. &n = Normal (&n)
   
   [extreal_pow_def]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀x a. x powr a = exp (a * ln x)
   
   [extreal_size_def]  Definition
      
      ⊢ extreal_size −∞ = 0 ∧ extreal_size +∞ = 0 ∧
        ∀a. extreal_size (Normal a) = 1
   
   [extreal_sqrt_def]  Definition
      
      ⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ sqrt +∞ = +∞
   
   [extreal_sup_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ (∀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]  Definition
      
      ⊢ ∀a b. open_interval a b = {x | a < x ∧ x < b}
   
   [open_intervals_def]  Definition
      
      ⊢ open_intervals = {open_interval a b | T}
   
   [rational_intervals_def]  Definition
      
      ⊢ rational_intervals = {open_interval a b | a ∈ ℚ ∧ b ∈ ℚ}
   
   [real_def]  Definition
      
      ⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r
   
   [real_set_def]  Definition
      
      ⊢ ∀s. real_set s = {real x | x ≠ +∞ ∧ x ≠ −∞ ∧ x ∈ s}
   
   [seq_sup_def]  Definition
      
      ⊢ (∀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
   
   [ABS_LE_HALF_POW2]  Theorem
      
      ⊢ ∀x y. abs (x * y) ≤ 1 / 2 * (x² + y²)
   
   [ADD_IN_Q]  Theorem
      
      ⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x + y ∈ ℚ
   
   [CEILING_LBOUND]  Theorem
      
      ⊢ ∀x. Normal x ≤ &ceiling (Normal x)
   
   [CEILING_UBOUND]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ &ceiling (Normal x) < Normal x + 1
   
   [CMUL_IN_Q]  Theorem
      
      ⊢ ∀z x. x ∈ ℚ ⇒ &z * x ∈ ℚ ∧ -&z * x ∈ ℚ
   
   [COUNTABLE_ENUM_Q]  Theorem
      
      ⊢ ∀c. COUNTABLE c ⇔ c = ∅ ∨ ∃f. c = IMAGE f ℚ
   
   [COUNTABLE_RATIONAL_INTERVALS]  Theorem
      
      ⊢ COUNTABLE rational_intervals
   
   [CROSS_COUNTABLE_UNIV]  Theorem
      
      ⊢ COUNTABLE (𝕌(:num) × 𝕌(:num))
   
   [DIV_IN_Q]  Theorem
      
      ⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ∧ y ≠ 0 ⇒ x / y ∈ ℚ
   
   [EXTREAL_ARCH]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x
   
   [EXTREAL_ARCH_POW]  Theorem
      
      ⊢ ∀x. x ≠ +∞ ⇒ ∃n. x < 2 pow n
   
   [EXTREAL_ARCH_POW_INV]  Theorem
      
      ⊢ ∀e. 0 < e ⇒ ∃n. Normal ((1 / 2) pow n) < e
   
   [EXTREAL_EQ_LADD]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y = x + z ⇔ y = z)
   
   [EXTREAL_EQ_RADD]  Theorem
      
      ⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x + z = y + z ⇔ x = y)
   
   [EXTREAL_PROD_IMAGE_DISJOINT_UNION]  Theorem
      
      ⊢ ∀s s'.
          FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
          ∀f. ∏ f (s ∪ s') = ∏ f s * ∏ f s'
   
   [EXTREAL_PROD_IMAGE_EMPTY]  Theorem
      
      ⊢ ∀f. ∏ f ∅ = 1
   
   [EXTREAL_PROD_IMAGE_EQ]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀f f'. (∀x. x ∈ s ⇒ f x = f' x) ⇒ ∏ f s = ∏ f' s
   
   [EXTREAL_PROD_IMAGE_IMAGE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀f'.
              INJ f' s (IMAGE f' s) ⇒ ∀f. ∏ f (IMAGE f' s) = ∏ (f ∘ f') s
   
   [EXTREAL_PROD_IMAGE_PAIR]  Theorem
      
      ⊢ ∀f a b. a ≠ b ⇒ ∏ f {a; b} = f a * f b
   
   [EXTREAL_PROD_IMAGE_PROPERTY]  Theorem
      
      ⊢ ∀f e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
   
   [EXTREAL_PROD_IMAGE_SING]  Theorem
      
      ⊢ ∀f e. ∏ f {e} = f e
   
   [EXTREAL_PROD_IMAGE_THM]  Theorem
      
      ⊢ ∀f. ∏ f ∅ = 1 ∧
            ∀e s. FINITE s ⇒ ∏ f (e INSERT s) = f e * ∏ f (s DELETE e)
   
   [EXTREAL_SUM_IMAGE_0]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = 0) ⇒ ∑ f s = 0
   
   [EXTREAL_SUM_IMAGE_ADD]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f. ∑ f ∅ = 0
   
   [EXTREAL_SUM_IMAGE_EQ]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∑ (λx. if x ∈ s then 1 else 0) s = &CARD s
   
   [EXTREAL_SUM_IMAGE_FINITE_CONST]  Theorem
      
      ⊢ ∀P. FINITE P ⇒ ∀f x. (∀y. y ∈ P ⇒ f y = x) ⇒ ∑ f P = &CARD P * x
   
   [EXTREAL_SUM_IMAGE_FINITE_SAME]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀s. s ≠ ∅ ∧ FINITE s ⇒
            ∑ (λx. if x ∈ s then (&CARD s)⁻¹ else 0) s = 1
   
   [EXTREAL_SUM_IMAGE_IN_IF]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f s t.
          FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
          ∑ f s ≤ ∑ f t
   
   [EXTREAL_SUM_IMAGE_NEG]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ 0) ⇒ ∑ f s ≤ 0
   
   [EXTREAL_SUM_IMAGE_NORMAL]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ ∑ (λx. Normal (f x)) s = Normal (∑ f s)
   
   [EXTREAL_SUM_IMAGE_NOT_INFTY]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞) ⇒ ∑ f s ≠ −∞
   
   [EXTREAL_SUM_IMAGE_NOT_POSINF]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ +∞) ⇒ ∑ f s ≠ +∞
   
   [EXTREAL_SUM_IMAGE_PERMUTES]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∑ f s
   
   [EXTREAL_SUM_IMAGE_POS_MEM_LE]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ s ⇒ f x ≤ ∑ f s
   
   [EXTREAL_SUM_IMAGE_POW]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f e. ∑ f {e} = f e
   
   [EXTREAL_SUM_IMAGE_SNEG]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < 0) ⇒ ∑ f s < 0
   
   [EXTREAL_SUM_IMAGE_SPOS]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < ∑ f s
   
   [EXTREAL_SUM_IMAGE_SUB]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∑ (λx. 0) s = 0
   
   [EXTREAL_SUM_IMAGE_ZERO_DIFF]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f n. (∀n. 0 ≤ f n) ⇒ ∑ f (count n) ≤ suminf f
   
   [EXTREAL_SUP_FUN_SEQ_IMAGE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x. x ∈ ℚ ∧ x ≠ 0 ⇒ 1 / x ∈ ℚ
   
   [MUL_IN_Q]  Theorem
      
      ⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x * y ∈ ℚ
   
   [NESTED_EXTREAL_SUM_IMAGE_REVERSE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀n. &n ∈ ℚ ∧ -&n ∈ ℚ
   
   [OPP_IN_Q]  Theorem
      
      ⊢ ∀x. x ∈ ℚ ⇒ -x ∈ ℚ
   
   [Q_COUNTABLE]  Theorem
      
      ⊢ COUNTABLE ℚ
   
   [Q_DENSE_IN_R]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ∃r. r ∈ ℚ ∧ x < r ∧ r < y
   
   [Q_DENSE_IN_R_LEMMA]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ ℚ ∧ x < r ∧ r < y
   
   [Q_INFINITE]  Theorem
      
      ⊢ INFINITE ℚ
   
   [Q_not_infty]  Theorem
      
      ⊢ ∀x. x ∈ ℚ ⇒ ∃y. x = Normal y
   
   [REAL_LE_MUL_EPSILON]  Theorem
      
      ⊢ ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
   
   [REAL_LE_RSUB_GE0]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇔ 0 ≤ y − x
   
   [SIMP_EXTREAL_ARCH]  Theorem
      
      ⊢ ∀x. x ≠ +∞ ⇒ ∃n. x ≤ &n
   
   [SIMP_EXTREAL_ARCH_NEG]  Theorem
      
      ⊢ ∀x. x ≠ −∞ ⇒ ∃n. -&n ≤ x
   
   [SUB_IN_Q]  Theorem
      
      ⊢ ∀x y. x ∈ ℚ ∧ y ∈ ℚ ⇒ x − y ∈ ℚ
   
   [abs_0]  Theorem
      
      ⊢ abs 0 = 0
   
   [abs_abs]  Theorem
      
      ⊢ ∀x. abs (abs x) = abs x
   
   [abs_bounds]  Theorem
      
      ⊢ ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k
   
   [abs_bounds_lt]  Theorem
      
      ⊢ ∀x k. abs x < k ⇔ -k < x ∧ x < k
   
   [abs_div]  Theorem
      
      ⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ 0 ⇒ abs (x / y) = abs x / abs y
   
   [abs_eq_0]  Theorem
      
      ⊢ ∀x. abs x = 0 ⇔ x = 0
   
   [abs_gt_0]  Theorem
      
      ⊢ ∀x. 0 < abs x ⇔ x ≠ 0
   
   [abs_le_0]  Theorem
      
      ⊢ ∀x. abs x ≤ 0 ⇔ x = 0
   
   [abs_le_half_pow2]  Theorem
      
      ⊢ ∀x y. abs (x * y) ≤ Normal (1 / 2) * (x² + y²)
   
   [abs_le_square_plus1]  Theorem
      
      ⊢ ∀x. abs x ≤ x² + 1
   
   [abs_max]  Theorem
      
      ⊢ ∀x. abs x = max x (-x)
   
   [abs_mul]  Theorem
      
      ⊢ ∀x y. abs (x * y) = abs x * abs y
   
   [abs_neg]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ abs x = -x
   
   [abs_not_infty]  Theorem
      
      ⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞
   
   [abs_pos]  Theorem
      
      ⊢ ∀x. 0 ≤ abs x
   
   [abs_pow2]  Theorem
      
      ⊢ ∀x. (abs x)² = x²
   
   [abs_pow_le_mono]  Theorem
      
      ⊢ ∀x n m. n ≤ m ⇒ abs x pow n ≤ 1 + abs x pow m
   
   [abs_refl]  Theorem
      
      ⊢ ∀x. abs x = x ⇔ 0 ≤ x
   
   [abs_triangle]  Theorem
      
      ⊢ ∀x y.
          x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y
   
   [abs_triangle_sub]  Theorem
      
      ⊢ ∀x y.
          x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (x − y)
   
   [abs_unbounds]  Theorem
      
      ⊢ ∀x k. 0 ≤ k ⇒ (k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x)
   
   [add2_sub2]  Theorem
      
      ⊢ ∀a b c d.
          a ≠ +∞ ∧ b ≠ +∞ ∧ c ≠ +∞ ∧ d ≠ +∞ ∧ a ≠ −∞ ∧ b ≠ −∞ ∧ c ≠ −∞ ∧
          d ≠ −∞ ⇒
          a − b + (c − d) = a + c − (b + d)
   
   [add_assoc]  Theorem
      
      ⊢ ∀x y z.
          x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ +∞ ⇒
          x + (y + z) = x + y + z
   
   [add_comm]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y = y + x
   
   [add_comm_normal]  Theorem
      
      ⊢ ∀x y. Normal x + y = y + Normal x
   
   [add_infty]  Theorem
      
      ⊢ (∀x. x ≠ −∞ ⇒ x + +∞ = +∞ ∧ +∞ + x = +∞) ∧
        ∀x. x ≠ +∞ ⇒ x + −∞ = −∞ ∧ −∞ + x = −∞
   
   [add_ldistrib]  Theorem
      
      ⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z
   
   [add_ldistrib_neg]  Theorem
      
      ⊢ ∀x y z. y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z
   
   [add_ldistrib_normal]  Theorem
      
      ⊢ ∀r y z.
          y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
          Normal r * (y + z) = Normal r * y + Normal r * z
   
   [add_ldistrib_normal2]  Theorem
      
      ⊢ ∀r y z.
          y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
          Normal r * (y + z) = Normal r * y + Normal r * z
   
   [add_ldistrib_pos]  Theorem
      
      ⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ⇒ x * (y + z) = x * y + x * z
   
   [add_lzero]  Theorem
      
      ⊢ ∀x. 0 + x = x
   
   [add_not_infty]  Theorem
      
      ⊢ ∀x y.
          (x ≠ −∞ ∧ y ≠ −∞ ⇒ x + y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y ≠ +∞)
   
   [add_pow2]  Theorem
      
      ⊢ ∀x y.
          x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒
          (x + y)² = x² + y² + 2 * x * y
   
   [add_pow2_pos]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ x ≠ +∞ ∧ 0 ≤ y ⇒ (x + y)² = x² + y² + 2 * x * y
   
   [add_rdistrib]  Theorem
      
      ⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ (y + z) * x = y * x + z * x
   
   [add_rdistrib_normal]  Theorem
      
      ⊢ ∀x y z.
          y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
          (y + z) * Normal x = y * Normal x + z * Normal x
   
   [add_rdistrib_normal2]  Theorem
      
      ⊢ ∀x y z.
          y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
          (y + z) * Normal x = y * Normal x + z * Normal x
   
   [add_rzero]  Theorem
      
      ⊢ ∀x. x + 0 = x
   
   [add_sub]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x + y − y = x
   
   [add_sub2]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ y + x − y = x
   
   [datatype_extreal]  Theorem
      
      ⊢ DATATYPE (extreal −∞ +∞ Normal)
   
   [div_add]  Theorem
      
      ⊢ ∀x y z.
          x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒
          x / z + y / z = (x + y) / z
   
   [div_add2]  Theorem
      
      ⊢ ∀x y z.
          (x ≠ +∞ ∧ y ≠ +∞ ∨ x ≠ −∞ ∧ y ≠ −∞) ∧ z ≠ 0 ∧ z ≠ +∞ ∧ z ≠ −∞ ⇒
          x / z + y / z = (x + y) / z
   
   [div_eq_mul_linv]  Theorem
      
      ⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = y⁻¹ * x
   
   [div_infty]  Theorem
      
      ⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ x / +∞ = 0 ∧ x / −∞ = 0
   
   [div_mul_refl]  Theorem
      
      ⊢ ∀x r. r ≠ 0 ⇒ x = x / Normal r * Normal r
   
   [div_not_infty]  Theorem
      
      ⊢ ∀x y. y ≠ 0 ⇒ Normal x / y ≠ +∞ ∧ Normal x / y ≠ −∞
   
   [div_one]  Theorem
      
      ⊢ ∀x. x / 1 = x
   
   [div_refl]  Theorem
      
      ⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x / x = 1
   
   [div_refl_pos]  Theorem
      
      ⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x / x = 1
   
   [entire]  Theorem
      
      ⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
   
   [eq_add_sub_switch]  Theorem
      
      ⊢ ∀a b c d.
          b ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ c ≠ +∞ ⇒
          (a + b = c + d ⇔ a − c = d − b)
   
   [eq_neg]  Theorem
      
      ⊢ ∀x y. -x = -y ⇔ x = y
   
   [eq_sub_ladd]  Theorem
      
      ⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x = y − z ⇔ x + z = y)
   
   [eq_sub_ladd_normal]  Theorem
      
      ⊢ ∀x y z. x = y − Normal z ⇔ x + Normal z = y
   
   [eq_sub_radd]  Theorem
      
      ⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y = z ⇔ x = z + y)
   
   [eq_sub_switch]  Theorem
      
      ⊢ ∀x y z. x = Normal z − y ⇔ y = Normal z − x
   
   [exp_0]  Theorem
      
      ⊢ exp 0 = 1
   
   [exp_pos]  Theorem
      
      ⊢ ∀x. 0 ≤ exp x
   
   [ext_mono_decreasing_suc]  Theorem
      
      ⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n
   
   [ext_mono_increasing_suc]  Theorem
      
      ⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)
   
   [ext_suminf_0]  Theorem
      
      ⊢ suminf (λn. 0) = 0
   
   [ext_suminf_2d]  Theorem
      
      ⊢ ∀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
   
   [ext_suminf_2d_full]  Theorem
      
      ⊢ ∀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
   
   [ext_suminf_add]  Theorem
      
      ⊢ ∀f g.
          (∀n. 0 ≤ f n ∧ 0 ≤ g n) ⇒
          suminf (λn. f n + g n) = suminf f + suminf g
   
   [ext_suminf_alt]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ⇒
            suminf (λx. f x) = sup {∑ (λi. f i) (count n) | n ∈ 𝕌(:num)}
   
   [ext_suminf_alt']  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ suminf (λx. f x) = sup {∑ f (count n) | n | T}
   
   [ext_suminf_cmul]  Theorem
      
      ⊢ ∀f c. 0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒ suminf (λn. c * f n) = c * suminf f
   
   [ext_suminf_cmul_alt]  Theorem
      
      ⊢ ∀f c.
          0 ≤ c ∧ (∀n. 0 ≤ f n) ∧ (∀n. f n < +∞) ⇒
          suminf (λn. Normal c * f n) = Normal c * suminf f
   
   [ext_suminf_eq]  Theorem
      
      ⊢ ∀f g. (∀n. f n = g n) ⇒ suminf f = suminf g
   
   [ext_suminf_eq_infty]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)) ⇒
            suminf f = +∞
   
   [ext_suminf_eq_infty_imp]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f = +∞ ⇒
            ∀e. e < +∞ ⇒ ∃n. e ≤ ∑ f (count n)
   
   [ext_suminf_lt_infty]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ suminf f < +∞ ⇒ ∀n. f n < +∞
   
   [ext_suminf_mono]  Theorem
      
      ⊢ ∀f g. (∀n. 0 ≤ g n) ∧ (∀n. g n ≤ f n) ⇒ suminf g ≤ suminf f
   
   [ext_suminf_pos]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
   
   [ext_suminf_posinf]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃n. f n = +∞) ⇒ suminf f = +∞
   
   [ext_suminf_real_suminf]  Theorem
      
      ⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒
            suminf (real ∘ g) = real (suminf g)
   
   [ext_suminf_sigma]  Theorem
      
      ⊢ ∀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']  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀r. 0 ≤ r ⇒ suminf (λn. if n = 0 then r else 0) = r
   
   [ext_suminf_sub]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f n.
          (∀n. 0 ≤ f n) ∧ (∀m. n ≤ m ⇒ f m = 0) ⇒ suminf f = ∑ f (count n)
   
   [ext_suminf_suminf]  Theorem
      
      ⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (λn. Normal (r n)) ≠ +∞ ⇒
            suminf (λn. Normal (r n)) = Normal (suminf r)
   
   [ext_suminf_suminf']  Theorem
      
      ⊢ ∀r. (∀n. 0 ≤ r n) ∧ suminf (Normal ∘ r) < +∞ ⇒
            suminf (Normal ∘ r) = Normal (suminf r)
   
   [ext_suminf_summable]  Theorem
      
      ⊢ ∀g. (∀n. 0 ≤ g n) ∧ suminf g < +∞ ⇒ summable (real ∘ g)
   
   [ext_suminf_sup_eq]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀f. (∀n. f n = 0) ⇒ suminf f = 0
   
   [extreal_11]  Theorem
      
      ⊢ ∀a a'. Normal a = Normal a' ⇔ a = a'
   
   [extreal_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2. ∃fn. fn −∞ = f0 ∧ fn +∞ = f1 ∧ ∀a. fn (Normal a) = f2 a
   
   [extreal_abs_def]  Theorem
      
      ⊢ abs (Normal x) = Normal (abs x) ∧ abs −∞ = +∞ ∧ abs +∞ = +∞
   
   [extreal_abs_ind]  Theorem
      
      ⊢ ∀P. (∀x. P (Normal x)) ∧ P −∞ ∧ P +∞ ⇒ ∀v. P v
   
   [extreal_add_def]  Theorem
      
      ⊢ Normal x + Normal y = Normal (x + y) ∧ Normal v0 + −∞ = −∞ ∧
        Normal v0 + +∞ = +∞ ∧ −∞ + Normal v1 = −∞ ∧ +∞ + Normal v1 = +∞ ∧
        −∞ + −∞ = −∞ ∧ +∞ + +∞ = +∞
   
   [extreal_add_eq]  Theorem
      
      ⊢ ∀x y. Normal x + Normal y = Normal (x + y)
   
   [extreal_add_ind]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ extreal_CASE x v v1 f = v' ⇔
        x = −∞ ∧ v = v' ∨ x = +∞ ∧ v1 = v' ∨ ∃r. x = Normal r ∧ f r = v'
   
   [extreal_cases]  Theorem
      
      ⊢ ∀x. x = −∞ ∨ x = +∞ ∨ ∃r. x = Normal r
   
   [extreal_distinct]  Theorem
      
      ⊢ −∞ ≠ +∞ ∧ (∀a. −∞ ≠ Normal a) ∧ ∀a. +∞ ≠ Normal a
   
   [extreal_div_eq]  Theorem
      
      ⊢ ∀x y. y ≠ 0 ⇒ Normal x / Normal y = Normal (x / y)
   
   [extreal_eq_zero]  Theorem
      
      ⊢ ∀x. Normal x = 0 ⇔ x = 0
   
   [extreal_induction]  Theorem
      
      ⊢ ∀P. P −∞ ∧ P +∞ ∧ (∀r. P (Normal r)) ⇒ ∀e. P e
   
   [extreal_inv_eq]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ (Normal x)⁻¹ = Normal x⁻¹
   
   [extreal_le_def]  Theorem
      
      ⊢ (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (−∞ ≤ v0 ⇔ T) ∧ (+∞ ≤ +∞ ⇔ T) ∧
        (Normal v5 ≤ +∞ ⇔ T) ∧ (+∞ ≤ −∞ ⇔ F) ∧ (Normal v6 ≤ −∞ ⇔ F) ∧
        (+∞ ≤ Normal v8 ⇔ F)
   
   [extreal_le_eq]  Theorem
      
      ⊢ ∀x y. Normal x ≤ Normal y ⇔ x ≤ y
   
   [extreal_le_ind]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x y. Normal x < Normal y ⇔ x < y
   
   [extreal_mean]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
   
   [extreal_mul_def]  Theorem
      
      ⊢ −∞ * −∞ = +∞ ∧ −∞ * +∞ = −∞ ∧ +∞ * −∞ = −∞ ∧ +∞ * +∞ = +∞ ∧
        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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀ee. ee = −∞ ∨ ee = +∞ ∨ ∃r. ee = Normal r
   
   [extreal_not_infty]  Theorem
      
      ⊢ ∀x. Normal x ≠ −∞ ∧ Normal x ≠ +∞
   
   [extreal_not_lt]  Theorem
      
      ⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
   
   [extreal_sub_add]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ y ≠ +∞ ∨ x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y = x + -y
   
   [extreal_sub_def]  Theorem
      
      ⊢ Normal x − Normal y = Normal (x − y) ∧ −∞ − Normal v0 = −∞ ∧
        +∞ − Normal v0 = +∞ ∧ Normal v1 − −∞ = +∞ ∧ Normal v2 − +∞ = −∞ ∧
        −∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞
   
   [extreal_sub_eq]  Theorem
      
      ⊢ ∀x y. Normal x − Normal y = Normal (x − y)
   
   [extreal_sub_ind]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ 4 * (1 / 4) = 1
   
   [fourths_between]  Theorem
      
      ⊢ ((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]  Theorem
      
      ⊢ ∀a n. 0 ≤ a ⇒ a pow n = a powr &n
   
   [half_between]  Theorem
      
      ⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
   
   [half_cancel]  Theorem
      
      ⊢ 2 * (1 / 2) = 1
   
   [half_not_infty]  Theorem
      
      ⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞
   
   [harmonic_series_pow_2]  Theorem
      
      ⊢ suminf (λn. (&SUC n)² ⁻¹) < +∞
   
   [inf_cminus]  Theorem
      
      ⊢ ∀f c.
          Normal c − inf (IMAGE f 𝕌(:α)) =
          sup (IMAGE (λn. Normal c − f n) 𝕌(:α))
   
   [inf_const]  Theorem
      
      ⊢ ∀x. inf (λy. y = x) = x
   
   [inf_const_alt]  Theorem
      
      ⊢ ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ x = z) ⇒ inf p = z
   
   [inf_const_over_set]  Theorem
      
      ⊢ ∀s k. s ≠ ∅ ⇒ inf (IMAGE (λx. k) s) = k
   
   [inf_empty]  Theorem
      
      ⊢ inf ∅ = +∞
   
   [inf_eq]  Theorem
      
      ⊢ ∀p x. inf p = x ⇔ (∀y. p y ⇒ x ≤ y) ∧ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
   
   [inf_eq']  Theorem
      
      ⊢ ∀p x.
          inf p = x ⇔ (∀y. y ∈ p ⇒ x ≤ y) ∧ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x
   
   [inf_le]  Theorem
      
      ⊢ ∀p x. inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
   
   [inf_le']  Theorem
      
      ⊢ ∀p x. inf p ≤ x ⇔ ∀y. (∀z. z ∈ p ⇒ y ≤ z) ⇒ y ≤ x
   
   [inf_le_imp]  Theorem
      
      ⊢ ∀p x. p x ⇒ inf p ≤ x
   
   [inf_le_imp']  Theorem
      
      ⊢ ∀p x. x ∈ p ⇒ inf p ≤ x
   
   [inf_lt]  Theorem
      
      ⊢ ∀P y. (∃x. P x ∧ x < y) ⇔ inf P < y
   
   [inf_lt']  Theorem
      
      ⊢ ∀P y. (∃x. x ∈ P ∧ x < y) ⇔ inf P < y
   
   [inf_lt_infty]  Theorem
      
      ⊢ ∀p. −∞ < inf p ⇒ ∀x. p x ⇒ −∞ < x
   
   [inf_min]  Theorem
      
      ⊢ ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ inf p = z
   
   [inf_minimal]  Theorem
      
      ⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ inf p ∈ p
   
   [inf_mono_subset]  Theorem
      
      ⊢ ∀p q. p ⊆ q ⇒ inf q ≤ inf p
   
   [inf_seq]  Theorem
      
      ⊢ ∀f l.
          mono_decreasing f ⇒
          (f ⟶ l ⇔ inf (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
   
   [inf_sing]  Theorem
      
      ⊢ ∀a. inf {a} = a
   
   [inf_suc]  Theorem
      
      ⊢ ∀f. (∀m n. m ≤ n ⇒ f n ≤ f m) ⇒
            inf (IMAGE (λn. f (SUC n)) 𝕌(:num)) = inf (IMAGE f 𝕌(:num))
   
   [inf_univ]  Theorem
      
      ⊢ inf 𝕌(:extreal) = −∞
   
   [infty_div]  Theorem
      
      ⊢ ∀r. 0 < r ⇒ +∞ / Normal r = +∞ ∧ −∞ / Normal r = −∞
   
   [inv_1over]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ x⁻¹ = 1 / x
   
   [inv_inj]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)
   
   [inv_le_antimono]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)
   
   [inv_lt_antimono]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)
   
   [inv_mul]  Theorem
      
      ⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x * y)⁻¹ = x⁻¹ * y⁻¹
   
   [inv_not_infty]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ≠ +∞ ∧ x⁻¹ ≠ −∞
   
   [inv_one]  Theorem
      
      ⊢ 1⁻¹ = 1
   
   [inv_pos]  Theorem
      
      ⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < 1 / x
   
   [inv_pos']  Theorem
      
      ⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < x⁻¹
   
   [inv_pos_eq]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ (0 < x⁻¹ ⇔ x ≠ +∞ ∧ 0 ≤ x)
   
   [ldiv_eq]  Theorem
      
      ⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x / z = y ⇔ x = y * z)
   
   [ldiv_le_imp]  Theorem
      
      ⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ∧ x ≤ y ⇒ x / z ≤ y / z
   
   [le_01]  Theorem
      
      ⊢ 0 ≤ 1
   
   [le_02]  Theorem
      
      ⊢ 0 ≤ 2
   
   [le_abs]  Theorem
      
      ⊢ ∀x. x ≤ abs x ∧ -x ≤ abs x
   
   [le_abs_bounds]  Theorem
      
      ⊢ ∀k x. k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x
   
   [le_add]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
   
   [le_add2]  Theorem
      
      ⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
   
   [le_add_neg]  Theorem
      
      ⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ x + y ≤ 0
   
   [le_addl_imp]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ⇒ y ≤ x + y
   
   [le_addr]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ x + y ⇔ 0 ≤ y)
   
   [le_addr_imp]  Theorem
      
      ⊢ ∀x y. 0 ≤ y ⇒ x ≤ x + y
   
   [le_antisym]  Theorem
      
      ⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
   
   [le_div]  Theorem
      
      ⊢ ∀y z. 0 ≤ y ∧ 0 < z ⇒ 0 ≤ y / Normal z
   
   [le_epsilon]  Theorem
      
      ⊢ ∀x y. (∀e. 0 < e ∧ e ≠ +∞ ⇒ x ≤ y + e) ⇒ x ≤ y
   
   [le_inf]  Theorem
      
      ⊢ ∀p x. x ≤ inf p ⇔ ∀y. p y ⇒ x ≤ y
   
   [le_inf']  Theorem
      
      ⊢ ∀p x. x ≤ inf p ⇔ ∀y. y ∈ p ⇒ x ≤ y
   
   [le_inf_epsilon_set]  Theorem
      
      ⊢ ∀P e.
          0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒
          ∃x. x ∈ P ∧ x ≤ inf P + e
   
   [le_infty]  Theorem
      
      ⊢ (∀x. −∞ ≤ x ∧ x ≤ +∞) ∧ (∀x. x ≤ −∞ ⇔ x = −∞) ∧ ∀x. +∞ ≤ x ⇔ x = +∞
   
   [le_inv]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ 0 ≤ x⁻¹
   
   [le_ladd]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y ≤ x + z ⇔ y ≤ z)
   
   [le_ladd_imp]  Theorem
      
      ⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z
   
   [le_ldiv]  Theorem
      
      ⊢ ∀x y z. 0 < x ⇒ (y ≤ z * Normal x ⇔ y / Normal x ≤ z)
   
   [le_lmul_imp]  Theorem
      
      ⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ z * x ≤ z * y
   
   [le_lneg]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ (-x ≤ y ⇔ 0 ≤ x + y)
   
   [le_lsub_imp]  Theorem
      
      ⊢ ∀x y z. y ≤ z ⇒ x − z ≤ x − y
   
   [le_lt]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y
   
   [le_max]  Theorem
      
      ⊢ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
   
   [le_max1]  Theorem
      
      ⊢ ∀x y. x ≤ max x y
   
   [le_max2]  Theorem
      
      ⊢ ∀x y. y ≤ max x y
   
   [le_min]  Theorem
      
      ⊢ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
   
   [le_mul]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
   
   [le_mul_epsilon]  Theorem
      
      ⊢ ∀x y. (∀z. 0 ≤ z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
   
   [le_mul_neg]  Theorem
      
      ⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y
   
   [le_neg]  Theorem
      
      ⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
   
   [le_not_infty]  Theorem
      
      ⊢ ∀x. (0 ≤ x ⇒ x ≠ −∞) ∧ (x ≤ 0 ⇒ x ≠ +∞)
   
   [le_num]  Theorem
      
      ⊢ ∀n. 0 ≤ &n
   
   [le_pow2]  Theorem
      
      ⊢ ∀x. 0 ≤ x²
   
   [le_radd]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x ≤ z + x ⇔ y ≤ z)
   
   [le_radd_imp]  Theorem
      
      ⊢ ∀x y z. y ≤ z ⇒ y + x ≤ z + x
   
   [le_rdiv]  Theorem
      
      ⊢ ∀x y z. 0 < x ⇒ (y * Normal x ≤ z ⇔ y ≤ z / Normal x)
   
   [le_refl]  Theorem
      
      ⊢ ∀x. x ≤ x
   
   [le_rmul_imp]  Theorem
      
      ⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ x * z ≤ y * z
   
   [le_rsub_imp]  Theorem
      
      ⊢ ∀x y z. x ≤ y ⇒ x − z ≤ y − z
   
   [le_sub_eq]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)
   
   [le_sub_eq2]  Theorem
      
      ⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ −∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)
   
   [le_sub_imp]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x
   
   [le_sub_imp2]  Theorem
      
      ⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x
   
   [le_sup]  Theorem
      
      ⊢ ∀p x. x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
   
   [le_sup']  Theorem
      
      ⊢ ∀p x. x ≤ sup p ⇔ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y
   
   [le_sup_imp]  Theorem
      
      ⊢ ∀p x. p x ⇒ x ≤ sup p
   
   [le_sup_imp']  Theorem
      
      ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
   
   [le_sup_imp2]  Theorem
      
      ⊢ ∀p z. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ z ≤ x) ⇒ z ≤ sup p
   
   [le_total]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y ≤ x
   
   [le_trans]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
   
   [let_add]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
   
   [let_add2]  Theorem
      
      ⊢ ∀w x y z. w ≠ −∞ ∧ w ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
   
   [let_add2_alt]  Theorem
      
      ⊢ ∀w x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
   
   [let_antisym]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y ≤ x)
   
   [let_mul]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
   
   [let_total]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y < x
   
   [let_trans]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
   
   [linv_uniq]  Theorem
      
      ⊢ ∀x y. x * y = 1 ⇒ x = y⁻¹
   
   [logr_not_infty]  Theorem
      
      ⊢ ∀x b. x ≠ −∞ ∧ x ≠ +∞ ⇒ logr b x ≠ −∞ ∧ logr b x ≠ +∞
   
   [lt_01]  Theorem
      
      ⊢ 0 < 1
   
   [lt_02]  Theorem
      
      ⊢ 0 < 2
   
   [lt_10]  Theorem
      
      ⊢ -1 < 0
   
   [lt_abs_bounds]  Theorem
      
      ⊢ ∀k x. k < abs x ⇔ x < -k ∨ k < x
   
   [lt_add]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
   
   [lt_add2]  Theorem
      
      ⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
   
   [lt_add_neg]  Theorem
      
      ⊢ ∀x y. x < 0 ∧ y < 0 ⇒ x + y < 0
   
   [lt_addl]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y < x + y ⇔ 0 < x)
   
   [lt_addr_imp]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y ⇒ x < x + y
   
   [lt_antisym]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y < x)
   
   [lt_div]  Theorem
      
      ⊢ ∀y z. 0 < y ∧ 0 < z ⇒ 0 < y / Normal z
   
   [lt_imp_le]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x ≤ y
   
   [lt_imp_ne]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x ≠ y
   
   [lt_inf_epsilon]  Theorem
      
      ⊢ ∀P e.
          0 < e ∧ (∃x. P x ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒ ∃x. P x ∧ x < inf P + e
   
   [lt_inf_epsilon_set]  Theorem
      
      ⊢ ∀P e.
          0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒
          ∃x. x ∈ P ∧ x < inf P + e
   
   [lt_infty]  Theorem
      
      ⊢ ∀x y.
          −∞ < Normal y ∧ Normal y < +∞ ∧ −∞ < +∞ ∧ ¬(x < −∞) ∧ ¬(+∞ < x) ∧
          (x ≠ +∞ ⇔ x < +∞) ∧ (x ≠ −∞ ⇔ −∞ < x)
   
   [lt_ladd]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y < x + z ⇔ y < z)
   
   [lt_ldiv]  Theorem
      
      ⊢ ∀x y z. 0 < z ⇒ (x / Normal z < y ⇔ x < y * Normal z)
   
   [lt_le]  Theorem
      
      ⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
   
   [lt_lmul]  Theorem
      
      ⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y < x * z ⇔ y < z)
   
   [lt_max_between]  Theorem
      
      ⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
   
   [lt_mul]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
   
   [lt_mul2]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≠ +∞ ∧ y1 ≠ +∞ ∧ x1 < x2 ∧ y1 < y2 ⇒
          x1 * y1 < x2 * y2
   
   [lt_mul_neg]  Theorem
      
      ⊢ ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y
   
   [lt_neg]  Theorem
      
      ⊢ ∀x y. -x < -y ⇔ y < x
   
   [lt_radd]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x < z + x ⇔ y < z)
   
   [lt_rdiv]  Theorem
      
      ⊢ ∀x y z. 0 < z ⇒ (x < y / Normal z ⇔ x * Normal z < y)
   
   [lt_rdiv_neg]  Theorem
      
      ⊢ ∀x y z. z < 0 ⇒ (y / Normal z < x ⇔ x * Normal z < y)
   
   [lt_refl]  Theorem
      
      ⊢ ∀x. ¬(x < x)
   
   [lt_rmul]  Theorem
      
      ⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z < y * z ⇔ x < y)
   
   [lt_sub]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)
   
   [lt_sub']  Theorem
      
      ⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)
   
   [lt_sub_imp]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ y + x < z ⇒ y < z − x
   
   [lt_sub_imp']  Theorem
      
      ⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ y + x < z ⇒ y < z − x
   
   [lt_sub_imp2]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x < z ⇒ y < z − x
   
   [lt_sup]  Theorem
      
      ⊢ ∀a s. a < sup s ⇔ ∃x. x ∈ s ∧ a < x
   
   [lt_total]  Theorem
      
      ⊢ ∀x y. x = y ∨ x < y ∨ y < x
   
   [lt_trans]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y < z ⇒ x < z
   
   [lte_add]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
   
   [lte_mul]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
   
   [lte_total]  Theorem
      
      ⊢ ∀x y. x < y ∨ y ≤ x
   
   [lte_trans]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
   
   [max_comm]  Theorem
      
      ⊢ ∀x y. max x y = max y x
   
   [max_fn_seq_compute]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀g n x. max_fn_seq g n x ≤ max_fn_seq g (SUC n) x
   
   [max_infty]  Theorem
      
      ⊢ ∀x. max x +∞ = +∞ ∧ max +∞ x = +∞ ∧ max −∞ x = x ∧ max x −∞ = x
   
   [max_le]  Theorem
      
      ⊢ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
   
   [max_le2_imp]  Theorem
      
      ⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
   
   [max_reduce]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y
   
   [max_refl]  Theorem
      
      ⊢ ∀x. max x x = x
   
   [min_comm]  Theorem
      
      ⊢ ∀x y. min x y = min y x
   
   [min_infty]  Theorem
      
      ⊢ ∀x. min x +∞ = x ∧ min +∞ x = x ∧ min −∞ x = −∞ ∧ min x −∞ = −∞
   
   [min_le]  Theorem
      
      ⊢ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
   
   [min_le1]  Theorem
      
      ⊢ ∀x y. min x y ≤ x
   
   [min_le2]  Theorem
      
      ⊢ ∀x y. min x y ≤ y
   
   [min_le2_imp]  Theorem
      
      ⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
   
   [min_le_between]  Theorem
      
      ⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x
   
   [min_reduce]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x
   
   [min_refl]  Theorem
      
      ⊢ ∀x. min x x = x
   
   [mul_assoc]  Theorem
      
      ⊢ ∀x y z. x * (y * z) = x * y * z
   
   [mul_comm]  Theorem
      
      ⊢ ∀x y. x * y = y * x
   
   [mul_div_refl]  Theorem
      
      ⊢ ∀x r. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < r ⇒ x = x * Normal r / Normal r
   
   [mul_infty]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞
   
   [mul_lcancel]  Theorem
      
      ⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (x * y = x * z ⇔ x = 0 ∨ y = z)
   
   [mul_le]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ y ≤ 0 ⇒ x * y ≤ 0
   
   [mul_le2]  Theorem
      
      ⊢ ∀x y. x ≤ 0 ∧ 0 ≤ y ⇒ x * y ≤ 0
   
   [mul_let]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ y < 0 ⇒ x * y ≤ 0
   
   [mul_linv]  Theorem
      
      ⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ * x = 1
   
   [mul_linv_pos]  Theorem
      
      ⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x⁻¹ * x = 1
   
   [mul_lneg]  Theorem
      
      ⊢ ∀x y. -x * y = -(x * y)
   
   [mul_lone]  Theorem
      
      ⊢ ∀x. 1 * x = x
   
   [mul_lposinf]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ +∞ * x = +∞
   
   [mul_lt]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ y < 0 ⇒ x * y < 0
   
   [mul_lt2]  Theorem
      
      ⊢ ∀x y. x < 0 ∧ 0 < y ⇒ x * y < 0
   
   [mul_lte]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ y ≤ 0 ⇒ x * y ≤ 0
   
   [mul_lzero]  Theorem
      
      ⊢ ∀x. 0 * x = 0
   
   [mul_not_infty]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ x * y ≠ −∞ ∧ x * y ≠ +∞
   
   [mul_rneg]  Theorem
      
      ⊢ ∀x y. x * -y = -(x * y)
   
   [mul_rone]  Theorem
      
      ⊢ ∀x. x * 1 = x
   
   [mul_rposinf]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ x * +∞ = +∞
   
   [mul_rzero]  Theorem
      
      ⊢ ∀x. x * 0 = 0
   
   [ne_01]  Theorem
      
      ⊢ 0 ≠ 1
   
   [ne_02]  Theorem
      
      ⊢ 0 ≠ 2
   
   [neg_0]  Theorem
      
      ⊢ -0 = 0
   
   [neg_add]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -(x + y) = -x + -y
   
   [neg_eq0]  Theorem
      
      ⊢ ∀x. -x = 0 ⇔ x = 0
   
   [neg_minus1]  Theorem
      
      ⊢ ∀x. -x = -1 * x
   
   [neg_mul2]  Theorem
      
      ⊢ ∀x y. -x * -y = x * y
   
   [neg_neg]  Theorem
      
      ⊢ ∀x. --x = x
   
   [neg_not_posinf]  Theorem
      
      ⊢ ∀x. x ≤ 0 ⇒ x ≠ +∞
   
   [neg_sub]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∨ y ≠ −∞ ∧ y ≠ +∞ ⇒ -(x − y) = y − x
   
   [normal_exp]  Theorem
      
      ⊢ ∀r. exp (Normal r) = Normal (exp r)
   
   [normal_inv_eq]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ Normal x⁻¹ = (Normal x)⁻¹
   
   [normal_powr]  Theorem
      
      ⊢ ∀r a. 0 < r ∧ 0 < a ⇒ Normal r powr Normal a = Normal (r powr a)
   
   [normal_real]  Theorem
      
      ⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ Normal (real x) = x
   
   [normal_real_set]  Theorem
      
      ⊢ ∀s. s ∩ IMAGE Normal 𝕌(:real) = IMAGE Normal (real_set s)
   
   [num_lt_infty]  Theorem
      
      ⊢ ∀n. &n < +∞
   
   [num_not_infty]  Theorem
      
      ⊢ ∀n. &n ≠ −∞ ∧ &n ≠ +∞
   
   [one_pow]  Theorem
      
      ⊢ ∀n. 1 pow n = 1
   
   [pos_not_neginf]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ x ≠ −∞
   
   [pos_summable]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃r. ∀n. ∑ f (count n) ≤ Normal r) ⇒
            suminf f < +∞
   
   [pow2_le_eq]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x² ≤ y²)
   
   [pow2_sqrt]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ sqrt x² = x
   
   [pow_0]  Theorem
      
      ⊢ ∀x. x pow 0 = 1
   
   [pow_1]  Theorem
      
      ⊢ ∀x. x pow 1 = x
   
   [pow_2]  Theorem
      
      ⊢ ∀x. x² = x * x
   
   [pow_add]  Theorem
      
      ⊢ ∀x n m. x pow (n + m) = x pow n * x pow m
   
   [pow_div]  Theorem
      
      ⊢ ∀n x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ (x / y) pow n = x pow n / y pow n
   
   [pow_half_pos_le]  Theorem
      
      ⊢ ∀n. 0 ≤ (1 / 2) pow (n + 1)
   
   [pow_half_pos_lt]  Theorem
      
      ⊢ ∀n. 0 < (1 / 2) pow (n + 1)
   
   [pow_half_ser]  Theorem
      
      ⊢ suminf (λn. (1 / 2) pow (n + 1)) = 1
   
   [pow_half_ser']  Theorem
      
      ⊢ suminf (λn. (1 / 2) pow SUC n) = 1
   
   [pow_half_ser_by_e]  Theorem
      
      ⊢ ∀e. 0 < e ∧ e ≠ +∞ ⇒ e = suminf (λn. e * (1 / 2) pow (n + 1))
   
   [pow_inv]  Theorem
      
      ⊢ ∀n y. y ≠ 0 ⇒ (y pow n)⁻¹ = y⁻¹ pow n
   
   [pow_le]  Theorem
      
      ⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n
   
   [pow_le_full]  Theorem
      
      ⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x pow n ≤ y pow n)
   
   [pow_le_mono]  Theorem
      
      ⊢ ∀x n m. 1 ≤ x ∧ n ≤ m ⇒ x pow n ≤ x pow m
   
   [pow_lt]  Theorem
      
      ⊢ ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n
   
   [pow_lt2]  Theorem
      
      ⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n
   
   [pow_minus1]  Theorem
      
      ⊢ ∀n. -1 pow (2 * n) = 1
   
   [pow_mul]  Theorem
      
      ⊢ ∀n x y. (x * y) pow n = x pow n * y pow n
   
   [pow_neg_odd]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
   
   [pow_not_infty]  Theorem
      
      ⊢ ∀n x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x pow n ≠ −∞ ∧ x pow n ≠ +∞
   
   [pow_pos_even]  Theorem
      
      ⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
   
   [pow_pos_le]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n
   
   [pow_pos_lt]  Theorem
      
      ⊢ ∀x n. 0 < x ⇒ 0 < x pow n
   
   [pow_zero]  Theorem
      
      ⊢ ∀n x. x pow SUC n = 0 ⇔ x = 0
   
   [pow_zero_imp]  Theorem
      
      ⊢ ∀n x. x pow n = 0 ⇒ x = 0
   
   [powr_0]  Theorem
      
      ⊢ ∀x. x powr 0 = 1
   
   [powr_pos]  Theorem
      
      ⊢ ∀x a. 0 ≤ x powr a
   
   [quotient_normal]  Theorem
      
      ⊢ ∀n m. m ≠ 0 ⇒ &n / &m = Normal (&n / &m)
   
   [rat_not_infty]  Theorem
      
      ⊢ ∀r. r ∈ ℚ ⇒ r ≠ −∞ ∧ r ≠ +∞
   
   [rdiv_eq]  Theorem
      
      ⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x = y / z ⇔ x * z = y)
   
   [real_normal]  Theorem
      
      ⊢ ∀x. real (Normal x) = x
   
   [rinv_uniq]  Theorem
      
      ⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹
   
   [seq_sup_compute]  Theorem
      
      ⊢ (∀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]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
   
   [sqrt_pos_le]  Theorem
      
      ⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x
   
   [sqrt_pos_lt]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ 0 < sqrt x
   
   [sqrt_pow2]  Theorem
      
      ⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x
   
   [sub_0]  Theorem
      
      ⊢ ∀x y. x − y = 0 ⇒ x = y
   
   [sub_add]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x − y + y = x
   
   [sub_add2]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ x + (y − x) = y
   
   [sub_eq_0]  Theorem
      
      ⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ x = y ⇒ x − y = 0
   
   [sub_infty]  Theorem
      
      ⊢ (∀x. x ≠ −∞ ⇒ x − −∞ = +∞) ∧ (∀x. x ≠ +∞ ⇒ x − +∞ = −∞) ∧
        (∀x. x ≠ +∞ ⇒ +∞ − x = +∞) ∧ ∀x. x ≠ −∞ ⇒ −∞ − x = −∞
   
   [sub_ldistrib]  Theorem
      
      ⊢ ∀x y z.
          x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
          x * (y − z) = x * y − x * z
   
   [sub_le_eq]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)
   
   [sub_le_eq2]  Theorem
      
      ⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ x ≠ −∞ ∧ z ≠ −∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)
   
   [sub_le_imp]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z
   
   [sub_le_imp2]  Theorem
      
      ⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z
   
   [sub_le_switch]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)
   
   [sub_le_switch2]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)
   
   [sub_le_zero]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x ≤ y ⇔ x − y ≤ 0)
   
   [sub_lneg]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -x − y = -(x + y)
   
   [sub_lt_eq]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x < z ⇔ y < z + x)
   
   [sub_lt_imp]  Theorem
      
      ⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y < z + x ⇒ y − x < z
   
   [sub_lt_imp2]  Theorem
      
      ⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y < z + x ⇒ y − x < z
   
   [sub_lt_zero]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x − y < 0
   
   [sub_lt_zero2]  Theorem
      
      ⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ∧ x − y < 0 ⇒ x < y
   
   [sub_lzero]  Theorem
      
      ⊢ ∀x. 0 − x = -x
   
   [sub_not_infty]  Theorem
      
      ⊢ ∀x y.
          (x ≠ −∞ ∧ y ≠ +∞ ⇒ x − y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y ≠ +∞)
   
   [sub_pow2]  Theorem
      
      ⊢ ∀x y.
          x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒
          (x − y)² = x² + y² − 2 * x * y
   
   [sub_rdistrib]  Theorem
      
      ⊢ ∀x y z.
          x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
          (x − y) * z = x * z − y * z
   
   [sub_refl]  Theorem
      
      ⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x − x = 0
   
   [sub_rneg]  Theorem
      
      ⊢ ∀c x. Normal c − -x = Normal c + x
   
   [sub_rzero]  Theorem
      
      ⊢ ∀x. x − 0 = x
   
   [sub_zero_le]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ y ⇔ 0 ≤ y − x)
   
   [sub_zero_lt]  Theorem
      
      ⊢ ∀x y. x < y ⇒ 0 < y − x
   
   [sub_zero_lt2]  Theorem
      
      ⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y − x ⇒ x < y
   
   [summable_ext_suminf]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ suminf (Normal ∘ f) < +∞
   
   [summable_ext_suminf_suminf]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒
            suminf (Normal ∘ f) = Normal (suminf f)
   
   [sup_add_mono]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀e s. 0 < e ∧ abs (sup s) ≠ +∞ ∧ s ≠ ∅ ⇒ ∃x. x ∈ s ∧ sup s − e < x
   
   [sup_cmul]  Theorem
      
      ⊢ ∀f c.
          0 ≤ c ⇒
          sup (IMAGE (λn. Normal c * f n) 𝕌(:α)) =
          Normal c * sup (IMAGE f 𝕌(:α))
   
   [sup_cmult]  Theorem
      
      ⊢ ∀f c.
          0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒
          sup (IMAGE (λn. c * f n) 𝕌(:α)) = c * sup (IMAGE f 𝕌(:α))
   
   [sup_comm]  Theorem
      
      ⊢ ∀f. sup {sup {f i j | j ∈ 𝕌(:num)} | i ∈ 𝕌(:num)} =
            sup {sup {f i j | i ∈ 𝕌(:num)} | j ∈ 𝕌(:num)}
   
   [sup_const]  Theorem
      
      ⊢ ∀x. sup (λy. y = x) = x
   
   [sup_const_alt]  Theorem
      
      ⊢ ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ x = z) ⇒ sup p = z
   
   [sup_const_alt']  Theorem
      
      ⊢ ∀p z. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ x = z) ⇒ sup p = z
   
   [sup_const_over_set]  Theorem
      
      ⊢ ∀s k. s ≠ ∅ ⇒ sup (IMAGE (λx. k) s) = k
   
   [sup_const_over_univ]  Theorem
      
      ⊢ ∀k. sup (IMAGE (λx. k) 𝕌(:α)) = k
   
   [sup_countable_seq]  Theorem
      
      ⊢ ∀A. A ≠ ∅ ⇒
            ∃f. IMAGE f 𝕌(:num) ⊆ A ∧ sup A = sup {f n | n ∈ 𝕌(:num)}
   
   [sup_empty]  Theorem
      
      ⊢ sup ∅ = −∞
   
   [sup_eq]  Theorem
      
      ⊢ ∀p x. sup p = x ⇔ (∀y. p y ⇒ y ≤ x) ∧ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
   
   [sup_eq']  Theorem
      
      ⊢ ∀p x.
          sup p = x ⇔ (∀y. y ∈ p ⇒ y ≤ x) ∧ ∀y. (∀z. z ∈ p ⇒ z ≤ y) ⇒ x ≤ y
   
   [sup_le]  Theorem
      
      ⊢ ∀p x. sup p ≤ x ⇔ ∀y. p y ⇒ y ≤ x
   
   [sup_le']  Theorem
      
      ⊢ ∀p x. sup p ≤ x ⇔ ∀y. y ∈ p ⇒ y ≤ x
   
   [sup_le_mono]  Theorem
      
      ⊢ ∀f z.
          (∀n. f n ≤ f (SUC n)) ∧ z < sup (IMAGE f 𝕌(:num)) ⇒ ∃n. z ≤ f n
   
   [sup_le_sup_imp]  Theorem
      
      ⊢ ∀p q. (∀x. p x ⇒ ∃y. q y ∧ x ≤ y) ⇒ sup p ≤ sup q
   
   [sup_le_sup_imp']  Theorem
      
      ⊢ ∀p q. (∀x. x ∈ p ⇒ ∃y. y ∈ q ∧ x ≤ y) ⇒ sup p ≤ sup q
   
   [sup_lt]  Theorem
      
      ⊢ ∀P y. (∃x. P x ∧ y < x) ⇔ y < sup P
   
   [sup_lt']  Theorem
      
      ⊢ ∀P y. (∃x. x ∈ P ∧ y < x) ⇔ y < sup P
   
   [sup_lt_epsilon]  Theorem
      
      ⊢ ∀P e.
          0 < e ∧ (∃x. P x ∧ x ≠ −∞) ∧ sup P ≠ +∞ ⇒ ∃x. P x ∧ sup P < x + e
   
   [sup_lt_infty]  Theorem
      
      ⊢ ∀p. sup p < +∞ ⇒ ∀x. p x ⇒ x < +∞
   
   [sup_max]  Theorem
      
      ⊢ ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ sup p = z
   
   [sup_maximal]  Theorem
      
      ⊢ ∀p. FINITE p ∧ p ≠ ∅ ⇒ sup p ∈ p
   
   [sup_mono]  Theorem
      
      ⊢ ∀p q.
          (∀n. p n ≤ q n) ⇒ sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))
   
   [sup_mono_ext]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀p q. p ⊆ q ⇒ sup p ≤ sup q
   
   [sup_num]  Theorem
      
      ⊢ sup (λx. ∃n. x = &n) = +∞
   
   [sup_seq]  Theorem
      
      ⊢ ∀f l.
          mono_increasing f ⇒
          (f ⟶ l ⇔ sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l)
   
   [sup_seq_countable_seq]  Theorem
      
      ⊢ ∀A g.
          A ≠ ∅ ⇒
          ∃f. IMAGE f 𝕌(:num) ⊆ IMAGE g A ∧
              sup {g n | n ∈ A} = sup {f n | n ∈ 𝕌(:num)}
   
   [sup_shift]  Theorem
      
      ⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
            ∀N. sup (IMAGE (λn. f (n + N)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))
   
   [sup_sing]  Theorem
      
      ⊢ ∀a. sup {a} = a
   
   [sup_suc]  Theorem
      
      ⊢ ∀f. (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
            sup (IMAGE (λn. f (SUC n)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num))
   
   [sup_sum_mono]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ sup 𝕌(:extreal) = +∞
   
   [third_cancel]  Theorem
      
      ⊢ 3 * (1 / 3) = 1
   
   [thirds_between]  Theorem
      
      ⊢ ((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]  Theorem
      
      ⊢ ∀x. x ≠ 0 ⇒ 0 / x = 0
   
   [zero_pow]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 0 pow n = 0
   
   [zero_rpow]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ 0 powr x = 0
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14