Structure extrealTheory
signature extrealTheory =
sig
type thm = Thm.thm
(* Definitions *)
val EXTREAL_SUM_IMAGE_DEF : thm
val Q_set : 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_product_def : thm
val ext_suminf_def : thm
val ext_tendsto_def : thm
val extreal_exp_def : thm
val extreal_inf_def : thm
val extreal_lg_def : thm
val extreal_lim_def : thm
val extreal_ln_def : thm
val extreal_logr_def : thm
val extreal_mr1_def : thm
val extreal_powr_def : thm
val extreal_sup_def : thm
val fn_minus_def : thm
val fn_plus_def : thm
val indicator_fn : thm
val max_fn_seq_def : thm
val nonneg_def : thm
val open_interval_def : thm
val open_intervals_def : thm
val rational_intervals_def : thm
val real_set_def : thm
(* Theorems *)
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 DROP_INDICATOR_FN : thm
val EXTREAL_ARCH : thm
val EXTREAL_ARCH_INV : thm
val EXTREAL_ARCH_INV' : thm
val EXTREAL_ARCH_POW2 : thm
val EXTREAL_ARCH_POW2_INV : thm
val EXTREAL_EQ_LADD : thm
val EXTREAL_EQ_RADD : thm
val EXTREAL_LIM : thm
val EXTREAL_LIM_EVENTUALLY : thm
val EXTREAL_LIM_SEQUENTIALLY : thm
val EXTREAL_PROD_IMAGE_0 : thm
val EXTREAL_PROD_IMAGE_1 : thm
val EXTREAL_PROD_IMAGE_COUNT_ONE : thm
val EXTREAL_PROD_IMAGE_COUNT_SUC : thm
val EXTREAL_PROD_IMAGE_COUNT_ZERO : 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_MONO : thm
val EXTREAL_PROD_IMAGE_NORMAL : thm
val EXTREAL_PROD_IMAGE_NOT_INFTY : thm
val EXTREAL_PROD_IMAGE_ONE : thm
val EXTREAL_PROD_IMAGE_PAIR : thm
val EXTREAL_PROD_IMAGE_POS : 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_ALT_FOLDR : thm
val EXTREAL_SUM_IMAGE_CMUL : thm
val EXTREAL_SUM_IMAGE_COUNT : thm
val EXTREAL_SUM_IMAGE_COUNT_ONE : thm
val EXTREAL_SUM_IMAGE_COUNT_SUC : thm
val EXTREAL_SUM_IMAGE_COUNT_ZERO : thm
val EXTREAL_SUM_IMAGE_CROSS_SYM : 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' : thm
val EXTREAL_SUM_IMAGE_EQ_CARD : thm
val EXTREAL_SUM_IMAGE_EQ_SHIFT : 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' : 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_OFFSET : 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 FN_ABS : thm
val FN_ABS' : thm
val FN_DECOMP : thm
val FN_DECOMP' : thm
val FN_MINUS_ABS_ZERO : thm
val FN_MINUS_ADD_LE : thm
val FN_MINUS_ALT : thm
val FN_MINUS_ALT' : thm
val FN_MINUS_CMUL : thm
val FN_MINUS_CMUL_full : thm
val FN_MINUS_FMUL : thm
val FN_MINUS_INFTY_IMP : thm
val FN_MINUS_LE_ABS : thm
val FN_MINUS_NOT_INFTY : thm
val FN_MINUS_POS : thm
val FN_MINUS_POS_ZERO : thm
val FN_MINUS_REDUCE : thm
val FN_MINUS_TO_PLUS : thm
val FN_MINUS_ZERO : thm
val FN_PLUS_ABS_SELF : thm
val FN_PLUS_ADD_LE : thm
val FN_PLUS_ALT : thm
val FN_PLUS_ALT' : thm
val FN_PLUS_CMUL : thm
val FN_PLUS_CMUL_full : thm
val FN_PLUS_FMUL : thm
val FN_PLUS_INFTY_IMP : thm
val FN_PLUS_LE_ABS : thm
val FN_PLUS_NEG_ZERO : thm
val FN_PLUS_NOT_INFTY : thm
val FN_PLUS_POS : thm
val FN_PLUS_POS_ID : thm
val FN_PLUS_REDUCE : thm
val FN_PLUS_REDUCE' : thm
val FN_PLUS_TO_MINUS : thm
val FN_PLUS_ZERO : thm
val INDICATOR_FN_ABS : thm
val INDICATOR_FN_ABS_MUL : thm
val INDICATOR_FN_CROSS : thm
val INDICATOR_FN_DIFF : thm
val INDICATOR_FN_DIFF_SPACE : thm
val INDICATOR_FN_EMPTY : thm
val INDICATOR_FN_INTER : thm
val INDICATOR_FN_INTER_MIN : thm
val INDICATOR_FN_LE_1 : thm
val INDICATOR_FN_MONO : thm
val INDICATOR_FN_MUL_INTER : thm
val INDICATOR_FN_NOT_INFTY : thm
val INDICATOR_FN_POS : thm
val INDICATOR_FN_SING_0 : thm
val INDICATOR_FN_SING_1 : thm
val INDICATOR_FN_UNION : thm
val INDICATOR_FN_UNION_MAX : thm
val INDICATOR_FN_UNION_MIN : 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 Q_set_def : 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_div_normal : 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_neg' : thm
val abs_neg_eq : thm
val abs_not_infty : thm
val abs_not_zero : thm
val abs_pos : thm
val abs_pow2 : thm
val abs_pow_le_mono : thm
val abs_real : thm
val abs_refl : thm
val abs_sub : thm
val abs_sub' : thm
val abs_triangle : thm
val abs_triangle_full : thm
val abs_triangle_neg : thm
val abs_triangle_neg_full : thm
val abs_triangle_sub : thm
val abs_triangle_sub' : thm
val abs_triangle_sub_full : thm
val abs_triangle_sub_full' : 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 add_sub_normal : thm
val conjugate_properties : thm
val div_add : thm
val div_add2 : thm
val div_eq_mul_linv : thm
val div_eq_mul_rinv : 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 div_sub : 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 eqle_trans : thm
val exp_0 : thm
val exp_add : thm
val exp_le_x : thm
val exp_le_x' : thm
val exp_mono_le : thm
val exp_neg : thm
val exp_pos : thm
val exp_pos_lt : thm
val ext_liminf_alt_limsup : thm
val ext_liminf_le_limsup : thm
val ext_liminf_pos : thm
val ext_limsup_alt_liminf : thm
val ext_limsup_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_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_eq_shift : thm
val ext_suminf_lt_infty : thm
val ext_suminf_mono : thm
val ext_suminf_nested : thm
val ext_suminf_offset : 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_sing_general : 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_0_simps : thm
val extreal_11 : thm
val extreal_1_simps : thm
val extreal_abs_def : thm
val extreal_add_def : thm
val extreal_add_eq : thm
val extreal_ainv_def : thm
val extreal_cases : thm
val extreal_dist_def : thm
val extreal_dist_ind : thm
val extreal_dist_ismet : thm
val extreal_dist_normal : thm
val extreal_distinct : thm
val extreal_div_def : thm
val extreal_div_eq : thm
val extreal_double : thm
val extreal_eq_zero : thm
val extreal_inv_def : thm
val extreal_inv_eq : thm
val extreal_le_def : thm
val extreal_le_eq : thm
val extreal_le_simps : thm
val extreal_lim_sequentially_eq : thm
val extreal_lim_sequentially_eq' : thm
val extreal_lt_def : thm
val extreal_lt_eq : thm
val extreal_lt_simps : thm
val extreal_max_def : thm
val extreal_mean : thm
val extreal_min_def : thm
val extreal_mr1_le_1 : thm
val extreal_mr1_normal : thm
val extreal_mr1_thm : thm
val extreal_mul_def : thm
val extreal_mul_eq : thm
val extreal_not_infty : thm
val extreal_not_lt : thm
val extreal_of_num_def : thm
val extreal_pow : thm
val extreal_pow_alt : thm
val extreal_pow_def : thm
val extreal_sqrt_def : thm
val extreal_sub : thm
val extreal_sub_add : thm
val extreal_sub_def : thm
val extreal_sub_eq : thm
val fn_minus : thm
val fn_minus_abs : thm
val fn_minus_mul_indicator : thm
val fn_plus : thm
val fn_plus_abs : thm
val fn_plus_alt : thm
val fn_plus_mul_indicator : thm
val fourth_cancel : thm
val fourths_between : thm
val gen_powr : thm
val geometric_series_pow : thm
val half_between : thm
val half_cancel : thm
val half_double : thm
val half_not_infty : thm
val harmonic_series_pow_2 : thm
val indicator_fn_def : thm
val indicator_fn_normal : thm
val indicator_fn_split : thm
val indicator_fn_suminf : thm
val ineq_imp : thm
val inf_cminus : thm
val inf_cmul : 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 : thm
val inf_mono_subset : thm
val inf_num : thm
val inf_seq : thm
val inf_sing : thm
val inf_suc : thm
val inf_univ : thm
val infty_div : thm
val infty_pow2 : thm
val infty_powr : thm
val inv_1over : thm
val inv_infty : thm
val inv_inj : thm
val inv_inv : thm
val inv_le_antimono : thm
val inv_le_antimono_imp : 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 inv_powr : 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 : 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 : 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_mul2 : thm
val le_mul_epsilon : thm
val le_mul_neg : thm
val le_neg : thm
val le_negl : thm
val le_negr : 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 : 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 leeq_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 lim_sequentially_imp_extreal_lim : thm
val linv_uniq : thm
val ln_1 : thm
val ln_inv : thm
val ln_mul : thm
val ln_neg : thm
val ln_neg_lt : thm
val ln_not_neginf : thm
val ln_pos : thm
val ln_pos_lt : 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 : 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' : 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_lmul_imp : thm
val lt_lsub_imp : thm
val lt_max : thm
val lt_max_between : thm
val lt_max_fn_seq : 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_rmul_imp : thm
val lt_rsub_imp : 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_0 : thm
val max_fn_seq_alt_sup : thm
val max_fn_seq_compute : thm
val max_fn_seq_cong : thm
val max_fn_seq_le : 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 monoidal_mul : thm
val mul_assoc : thm
val mul_comm : thm
val mul_div_refl : thm
val mul_infty : 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_powr : thm
val mul_rcancel : 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 neutral_mul : thm
val nonneg_abs : thm
val nonneg_fn_abs : thm
val nonneg_fn_minus : thm
val nonneg_fn_plus : thm
val normal_0 : thm
val normal_1 : thm
val normal_exp : thm
val normal_inv_eq : thm
val normal_minus1 : 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 one_powr : 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_2_abs : thm
val pow_add : thm
val pow_ainv_even : thm
val pow_ainv_odd : thm
val pow_div : thm
val pow_eq : thm
val pow_even_le : 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_pow : thm
val pow_zero : thm
val pow_zero_imp : thm
val powr_0 : thm
val powr_1 : thm
val powr_add : thm
val powr_eq_0 : thm
val powr_ge_1 : thm
val powr_infty : thm
val powr_le_eq : thm
val powr_mono_eq : thm
val powr_pos : thm
val powr_pos_lt : thm
val powr_powr : thm
val quotient_normal : thm
val rat_not_infty : thm
val rdiv_eq : thm
val real_0 : thm
val real_def : thm
val real_normal : thm
val rinv_uniq : thm
val sqrt_0 : thm
val sqrt_1 : thm
val sqrt_le_n : thm
val sqrt_le_x : thm
val sqrt_mono_le : thm
val sqrt_mul : thm
val sqrt_pos_le : thm
val sqrt_pos_lt : thm
val sqrt_pos_ne : thm
val sqrt_pow2 : thm
val sqrt_powr : thm
val sub_0 : thm
val sub_add : thm
val sub_add2 : thm
val sub_add_normal : 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_sub_imp : 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_insert : 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_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 x_half_half : thm
val young_inequality : thm
val zero_div : thm
val zero_pow : thm
val zero_rpow : thm
val extreal_grammars : type_grammar.grammar * term_grammar.grammar
(*
[extreal_base] Parent theory of "extreal"
[real_of_rat] Parent theory of "extreal"
[transc] Parent theory of "extreal"
[EXTREAL_SUM_IMAGE_DEF] Definition
⊢ ∀f s. ∑ f s = ITSET (λe acc. f e + acc) s 0
[Q_set] Definition
⊢ ℚ꙳ = IMAGE Normal ℚ
[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_product_def] Definition
⊢ ext_product = iterate $*
[ext_suminf_def] Definition
⊢ ∀f. (∀n. 0 ≤ f n) ⇒
suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))
[ext_tendsto_def] Definition
⊢ ∀f l net.
(f --> l) net ⇔
∀e. 0 < e ⇒ eventually (λx. dist extreal_mr1 (f x,l) < e) net
[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_lg_def] Definition
⊢ ∀x. lg x = logr 2 x
[extreal_lim_def] Definition
⊢ ∀net f. lim net f = @l. (f --> l) net
[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_mr1_def] Definition
⊢ extreal_mr1 = metric (UNCURRY extreal_dist)
[extreal_powr_def] Definition
⊢ ∀x a. x powr a = exp (a * ln x)
[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)))
[fn_minus_def] Definition
⊢ ∀f. f⁻ = (λx. if f x < 0 then -f x else 0)
[fn_plus_def] Definition
⊢ ∀f. f⁺ = (λx. if 0 < f x then f x else 0)
[indicator_fn] Definition
⊢ ∀s. 𝟙 s = Normal ∘ indicator s
[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)
[nonneg_def] Definition
⊢ ∀f. nonneg f ⇔ ∀x. 0 ≤ f 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_set_def] Definition
⊢ ∀s. real_set s = {real x | x ≠ +∞ ∧ x ≠ −∞ ∧ x ∈ s}
[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 ∈ ℚ꙳
[DROP_INDICATOR_FN] Theorem
⊢ ∀s x. 𝟙 s x = if x ∈ s then 1 else 0
[EXTREAL_ARCH] Theorem
⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x
[EXTREAL_ARCH_INV] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x
[EXTREAL_ARCH_INV'] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ ≤ x
[EXTREAL_ARCH_POW2] Theorem
⊢ ∀x. x ≠ +∞ ⇒ ∃n. x < 2 pow n
[EXTREAL_ARCH_POW2_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_LIM] Theorem
⊢ ∀f l net.
(f --> l) net ⇔
trivial_limit net ∨
∀e. 0 < e ⇒
∃y. (∃x. netord net x y) ∧
∀x. netord net x y ⇒ dist extreal_mr1 (f x,l) < e
[EXTREAL_LIM_EVENTUALLY] Theorem
⊢ ∀net f l. eventually (λx. f x = l) net ⇒ (f --> l) net
[EXTREAL_LIM_SEQUENTIALLY] Theorem
⊢ ∀f l.
(f --> l) sequentially ⇔
∀e. 0 < e ⇒ ∃N. ∀n. N ≤ n ⇒ dist extreal_mr1 (f n,l) < e
[EXTREAL_PROD_IMAGE_0] Theorem
⊢ ∀f s. FINITE s ∧ (∃x. x ∈ s ∧ f x = 0) ⇒ ∏ f s = 0
[EXTREAL_PROD_IMAGE_1] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = 1) ⇒ ∏ f s = 1
[EXTREAL_PROD_IMAGE_COUNT_ONE] Theorem
⊢ ∀f. ∏ f (count 1) = f 0
[EXTREAL_PROD_IMAGE_COUNT_SUC] Theorem
⊢ ∀f n. ∏ f (count (SUC n)) = ∏ f (count n) * f n
[EXTREAL_PROD_IMAGE_COUNT_ZERO] Theorem
⊢ ∀f. ∏ f (count 0) = 1
[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 f f'. (∀x. x ∈ s ⇒ f x = f' x) ⇒ ∏ f s = ∏ f' s
[EXTREAL_PROD_IMAGE_IMAGE] Theorem
⊢ ∀s f'. INJ f' s (IMAGE f' s) ⇒ ∀f. ∏ f (IMAGE f' s) = ∏ (f ∘ f') s
[EXTREAL_PROD_IMAGE_MONO] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒ ∏ f s ≤ ∏ g s
[EXTREAL_PROD_IMAGE_NORMAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∏ (λx. Normal (f x)) s = Normal (∏ f s)
[EXTREAL_PROD_IMAGE_NOT_INFTY] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ −∞ ∧ f x ≠ +∞) ⇒
∏ f s ≠ −∞ ∧ ∏ f s ≠ +∞
[EXTREAL_PROD_IMAGE_ONE] Theorem
⊢ ∀s. FINITE s ⇒ ∏ (λx. 1) s = 1
[EXTREAL_PROD_IMAGE_PAIR] Theorem
⊢ ∀f a b. a ≠ b ⇒ ∏ f {a; b} = f a * f b
[EXTREAL_PROD_IMAGE_POS] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ ∏ f s
[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_ALT_FOLDR] Theorem
⊢ ∀f s.
FINITE s ⇒
∑ f s = FOLDR (λe acc. f e + acc) 0 (REVERSE (SET_TO_LIST 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_COUNT_ONE] Theorem
⊢ ∀f. ∑ f (count 1) = f 0
[EXTREAL_SUM_IMAGE_COUNT_SUC] Theorem
⊢ ∀f n.
(∀m. m ≤ n ⇒ f m ≠ −∞) ∨ (∀m. m ≤ n ⇒ f m ≠ +∞) ⇒
∑ f (count (SUC n)) = ∑ f (count n) + f n
[EXTREAL_SUM_IMAGE_COUNT_ZERO] Theorem
⊢ ∀f. ∑ f (count 0) = 0
[EXTREAL_SUM_IMAGE_CROSS_SYM] Theorem
⊢ ∀f s1 s2.
FINITE s1 ∧ FINITE s2 ∧
((∀s. s ∈ s1 × s2 ⇒ f s ≠ −∞) ∨ ∀s. s ∈ s1 × s2 ⇒ f s ≠ +∞) ⇒
∑ (λ(x,y). f (x,y)) (s1 × s2) = ∑ (λ(y,x). f (x,y)) (s2 × s1)
[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'] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x = g x) ⇒ ∑ f s = ∑ g s
[EXTREAL_SUM_IMAGE_EQ_CARD] Theorem
⊢ ∀s. FINITE s ⇒ ∑ (λx. if x ∈ s then 1 else 0) s = &CARD s
[EXTREAL_SUM_IMAGE_EQ_SHIFT] Theorem
⊢ ∀f g N.
(∀n. n < N ⇒ g n = 0) ∧ (∀n. 0 ≤ f n ∧ f n = g (n + N)) ⇒
∀n. ∑ f (count n) = ∑ g (count (n + N))
[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'] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ ∑ f s ≤ ∑ g 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_OFFSET] Theorem
⊢ ∀f m n.
m ≤ n ∧ (∀n. 0 ≤ f n) ⇒
∑ f (count n) = ∑ f (count m) + ∑ (λi. f (i + m)) (count (n − m))
[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
[FN_ABS] Theorem
⊢ ∀f x. (abs ∘ f) x = f⁺ x + f⁻ x
[FN_ABS'] Theorem
⊢ ∀f. abs ∘ f = (λx. f⁺ x + f⁻ x)
[FN_DECOMP] Theorem
⊢ ∀f x. f x = f⁺ x − f⁻ x
[FN_DECOMP'] Theorem
⊢ ∀f. f = (λx. f⁺ x − f⁻ x)
[FN_MINUS_ABS_ZERO] Theorem
⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)
[FN_MINUS_ADD_LE] Theorem
⊢ ∀f g x.
f x ≠ −∞ ∧ g x ≠ −∞ ∨ f x ≠ +∞ ∧ g x ≠ +∞ ⇒
(λx. f x + g x)⁻ x ≤ f⁻ x + g⁻ x
[FN_MINUS_ALT] Theorem
⊢ ∀f. f⁻ = (λx. -min (f x) 0)
[FN_MINUS_ALT'] Theorem
⊢ ∀f. f⁻ = (λx. -min 0 (f x))
[FN_MINUS_CMUL] Theorem
⊢ ∀f c.
(0 ≤ c ⇒ (λx. Normal c * f x)⁻ = (λx. Normal c * f⁻ x)) ∧
(c ≤ 0 ⇒ (λx. Normal c * f x)⁻ = (λx. -Normal c * f⁺ x))
[FN_MINUS_CMUL_full] Theorem
⊢ ∀f c.
(0 ≤ c ⇒ (λx. c * f x)⁻ = (λx. c * f⁻ x)) ∧
(c ≤ 0 ⇒ (λx. c * f x)⁻ = (λx. -c * f⁺ x))
[FN_MINUS_FMUL] Theorem
⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁻ = (λx. c x * f⁻ x)
[FN_MINUS_INFTY_IMP] Theorem
⊢ ∀f x. f⁻ x = +∞ ⇒ f⁺ x = 0
[FN_MINUS_LE_ABS] Theorem
⊢ ∀f x. f⁻ x ≤ abs (f x)
[FN_MINUS_NOT_INFTY] Theorem
⊢ ∀f x. f x ≠ −∞ ⇒ f⁻ x ≠ +∞
[FN_MINUS_POS] Theorem
⊢ ∀g x. 0 ≤ g⁻ x
[FN_MINUS_POS_ZERO] Theorem
⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁻ = (λx. 0)
[FN_MINUS_REDUCE] Theorem
⊢ ∀f x. 0 ≤ f x ⇒ f⁻ x = 0
[FN_MINUS_TO_PLUS] Theorem
⊢ ∀f. (λx. -f x)⁻ = f⁺
[FN_MINUS_ZERO] Theorem
⊢ (λx. 0)⁻ = (λx. 0)
[FN_PLUS_ABS_SELF] Theorem
⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f
[FN_PLUS_ADD_LE] Theorem
⊢ ∀f g x. (λx. f x + g x)⁺ x ≤ f⁺ x + g⁺ x
[FN_PLUS_ALT] Theorem
⊢ ∀f. f⁺ = (λx. max (f x) 0)
[FN_PLUS_ALT'] Theorem
⊢ ∀f. f⁺ = (λx. max 0 (f x))
[FN_PLUS_CMUL] Theorem
⊢ ∀f c.
(0 ≤ c ⇒ (λx. Normal c * f x)⁺ = (λx. Normal c * f⁺ x)) ∧
(c ≤ 0 ⇒ (λx. Normal c * f x)⁺ = (λx. -Normal c * f⁻ x))
[FN_PLUS_CMUL_full] Theorem
⊢ ∀f c.
(0 ≤ c ⇒ (λx. c * f x)⁺ = (λx. c * f⁺ x)) ∧
(c ≤ 0 ⇒ (λx. c * f x)⁺ = (λx. -c * f⁻ x))
[FN_PLUS_FMUL] Theorem
⊢ ∀f c. (∀x. 0 ≤ c x) ⇒ (λx. c x * f x)⁺ = (λx. c x * f⁺ x)
[FN_PLUS_INFTY_IMP] Theorem
⊢ ∀f x. f⁺ x = +∞ ⇒ f⁻ x = 0
[FN_PLUS_LE_ABS] Theorem
⊢ ∀f x. f⁺ x ≤ abs (f x)
[FN_PLUS_NEG_ZERO] Theorem
⊢ ∀g. (∀x. g x ≤ 0) ⇒ g⁺ = (λx. 0)
[FN_PLUS_NOT_INFTY] Theorem
⊢ ∀f x. f x ≠ +∞ ⇒ f⁺ x ≠ +∞
[FN_PLUS_POS] Theorem
⊢ ∀g x. 0 ≤ g⁺ x
[FN_PLUS_POS_ID] Theorem
⊢ ∀g. (∀x. 0 ≤ g x) ⇒ g⁺ = g
[FN_PLUS_REDUCE] Theorem
⊢ ∀f x. 0 ≤ f x ⇒ f⁺ x = f x
[FN_PLUS_REDUCE'] Theorem
⊢ ∀f x. f x ≤ 0 ⇒ f⁺ x = 0
[FN_PLUS_TO_MINUS] Theorem
⊢ ∀f. (λx. -f x)⁺ = f⁻
[FN_PLUS_ZERO] Theorem
⊢ (λx. 0)⁺ = (λx. 0)
[INDICATOR_FN_ABS] Theorem
⊢ ∀s. abs ∘ 𝟙 s = 𝟙 s
[INDICATOR_FN_ABS_MUL] Theorem
⊢ ∀f s. abs ∘ (λx. f x * 𝟙 s x) = (λx. (abs ∘ f) x * 𝟙 s x)
[INDICATOR_FN_CROSS] Theorem
⊢ ∀s t x y. 𝟙 (s × t) (x,y) = 𝟙 s x * 𝟙 t y
[INDICATOR_FN_DIFF] Theorem
⊢ ∀A B. 𝟙 (A DIFF B) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)
[INDICATOR_FN_DIFF_SPACE] Theorem
⊢ ∀A B sp.
A ⊆ sp ∧ B ⊆ sp ⇒ 𝟙 (A ∩ (sp DIFF B)) = (λt. 𝟙 A t − 𝟙 (A ∩ B) t)
[INDICATOR_FN_EMPTY] Theorem
⊢ ∀x. 𝟙 ∅ x = 0
[INDICATOR_FN_INTER] Theorem
⊢ ∀A B. 𝟙 (A ∩ B) = (λt. 𝟙 A t * 𝟙 B t)
[INDICATOR_FN_INTER_MIN] Theorem
⊢ ∀A B. 𝟙 (A ∩ B) = (λt. min (𝟙 A t) (𝟙 B t))
[INDICATOR_FN_LE_1] Theorem
⊢ ∀s x. 𝟙 s x ≤ 1
[INDICATOR_FN_MONO] Theorem
⊢ ∀s t x. s ⊆ t ⇒ 𝟙 s x ≤ 𝟙 t x
[INDICATOR_FN_MUL_INTER] Theorem
⊢ ∀A B. (λt. 𝟙 A t * 𝟙 B t) = (λt. 𝟙 (A ∩ B) t)
[INDICATOR_FN_NOT_INFTY] Theorem
⊢ ∀s x. 𝟙 s x ≠ −∞ ∧ 𝟙 s x ≠ +∞
[INDICATOR_FN_POS] Theorem
⊢ ∀s x. 0 ≤ 𝟙 s x
[INDICATOR_FN_SING_0] Theorem
⊢ ∀x y. x ≠ y ⇒ 𝟙 {x} y = 0
[INDICATOR_FN_SING_1] Theorem
⊢ ∀x y. x = y ⇒ 𝟙 {x} y = 1
[INDICATOR_FN_UNION] Theorem
⊢ ∀A B. 𝟙 (A ∪ B) = (λt. 𝟙 A t + 𝟙 B t − 𝟙 (A ∩ B) t)
[INDICATOR_FN_UNION_MAX] Theorem
⊢ ∀A B. 𝟙 (A ∪ B) = (λt. max (𝟙 A t) (𝟙 B t))
[INDICATOR_FN_UNION_MIN] Theorem
⊢ ∀A B. 𝟙 (A ∪ B) = (λt. min (𝟙 A t + 𝟙 B t) 1)
[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
[Q_set_def] Theorem
⊢ ℚ꙳ =
{x | ∃a b. x = &a / &b ∧ 0 < &b} ∪
{x | ∃a b. x = -(&a / &b) ∧ 0 < &b}
[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_div_normal] Theorem
⊢ ∀x y. y ≠ 0 ⇒ abs (x / Normal y) = abs x / Normal (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_neg'] Theorem
⊢ ∀x. x ≤ 0 ⇒ abs x = -x
[abs_neg_eq] Theorem
⊢ ∀x. abs (-x) = abs x
[abs_not_infty] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞
[abs_not_zero] Theorem
⊢ ∀x. abs x ≠ 0 ⇔ x ≠ 0
[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_real] Theorem
⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs (real x) = real (abs x)
[abs_refl] Theorem
⊢ ∀x. abs x = x ⇔ 0 ≤ x
[abs_sub] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) = abs (y − x)
[abs_sub'] Theorem
⊢ ∀x y. abs (x − y) = abs (y − x)
[abs_triangle] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y
[abs_triangle_full] Theorem
⊢ ∀x y. abs (x + y) ≤ abs x + abs y
[abs_triangle_neg] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) ≤ abs x + abs y
[abs_triangle_neg_full] Theorem
⊢ ∀x 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_triangle_sub'] Theorem
⊢ ∀x y.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (y − x)
[abs_triangle_sub_full] Theorem
⊢ ∀x y. abs x ≤ abs y + abs (x − y)
[abs_triangle_sub_full'] Theorem
⊢ ∀x y. abs x ≤ abs y + abs (y − x)
[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 + 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
[add_sub_normal] Theorem
⊢ ∀x r. x + Normal r − Normal r = x
[conjugate_properties] Theorem
⊢ ∀p q.
0 < p ∧ 0 < q ∧ p⁻¹ + q⁻¹ = 1 ⇒
1 ≤ p ∧ 1 ≤ q ∧ (p = 1 ⇔ q = +∞) ∧ (q = 1 ⇔ p = +∞)
[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_eq_mul_rinv] Theorem
⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = x * y⁻¹
[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
[div_sub] Theorem
⊢ ∀x y z.
x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒
x / z − y / z = (x − y) / z
[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
[eqle_trans] Theorem
⊢ ∀x y z. x = y ∧ y ≤ z ⇒ x ≤ z
[exp_0] Theorem
⊢ exp 0 = 1
[exp_add] Theorem
⊢ ∀x y.
x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ exp (x + y) = exp x * exp y
[exp_le_x] Theorem
⊢ ∀x. 1 + x ≤ exp x
[exp_le_x'] Theorem
⊢ ∀x. 1 − x ≤ exp (-x)
[exp_mono_le] Theorem
⊢ ∀x y. exp x ≤ exp y ⇔ x ≤ y
[exp_neg] Theorem
⊢ ∀x. x ≠ −∞ ⇒ exp (-x) = (exp x)⁻¹
[exp_pos] Theorem
⊢ ∀x. 0 ≤ exp x
[exp_pos_lt] Theorem
⊢ ∀x. x ≠ −∞ ⇒ 0 < exp x
[ext_liminf_alt_limsup] Theorem
⊢ ∀a. liminf a = -limsup (numeric_negate ∘ a)
[ext_liminf_le_limsup] Theorem
⊢ ∀a. liminf a ≤ limsup a
[ext_liminf_pos] Theorem
⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ liminf a
[ext_limsup_alt_liminf] Theorem
⊢ ∀a. limsup a = -liminf (numeric_negate ∘ a)
[ext_limsup_pos] Theorem
⊢ ∀a. (∀n. 0 ≤ a n) ⇒ 0 ≤ limsup a
[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_add'] Theorem
⊢ ∀f g h.
(∀n. 0 ≤ f n) ∧ (∀n. 0 ≤ g n) ∧ (∀n. h n = f n + g n) ⇒
suminf h = 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_eq_shift] Theorem
⊢ ∀f g N.
(∀n. n < N ⇒ g n = 0) ∧ (∀n. 0 ≤ f n ∧ f n = g (n + N)) ⇒
suminf f = suminf g
[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_nested] Theorem
⊢ ∀f. (∀m n. 0 ≤ f m n) ⇒
suminf (λn. suminf (λm. f m n)) =
suminf (λm. suminf (λn. f m n))
[ext_suminf_offset] Theorem
⊢ ∀f m.
(∀n. 0 ≤ f n) ⇒ suminf f = ∑ f (count m) + suminf (λi. f (i + m))
[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_sing_general] Theorem
⊢ ∀m r. 0 ≤ r ⇒ suminf (λn. if n = m 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 ⇒ f m i ≤ f n i) ∧ (∀n i. 0 ≤ f n i) ⇒
suminf (λi. sup {f n i | n ∈ 𝕌(:num)}) =
sup {suminf (λi. f n i) | n ∈ 𝕌(:num)}
[ext_suminf_zero] Theorem
⊢ ∀f. (∀n. f n = 0) ⇒ suminf f = 0
[extreal_0_simps] Theorem
⊢ (0 ≤ +∞ ⇔ T) ∧ (0 < +∞ ⇔ T) ∧ (+∞ ≤ 0 ⇔ F) ∧ (+∞ < 0 ⇔ F) ∧
(0 = +∞ ⇔ F) ∧ (+∞ = 0 ⇔ F) ∧ (0 ≤ −∞ ⇔ F) ∧ (0 < −∞ ⇔ F) ∧
(−∞ ≤ 0 ⇔ T) ∧ (−∞ < 0 ⇔ T) ∧ (0 = −∞ ⇔ F) ∧ (−∞ = 0 ⇔ F) ∧
(∀r. 0 ≤ Normal r ⇔ 0 ≤ r) ∧ (∀r. 0 < Normal r ⇔ 0 < r) ∧
(∀r. 0 = Normal r ⇔ r = 0) ∧ (∀r. Normal r ≤ 0 ⇔ r ≤ 0) ∧
(∀r. Normal r < 0 ⇔ r < 0) ∧ ∀r. Normal r = 0 ⇔ r = 0
[extreal_11] Theorem
⊢ ∀a a'. Normal a = Normal a' ⇔ a = a'
[extreal_1_simps] Theorem
⊢ (1 ≤ +∞ ⇔ T) ∧ (1 < +∞ ⇔ T) ∧ (+∞ ≤ 1 ⇔ F) ∧ (+∞ < 1 ⇔ F) ∧
(1 = +∞ ⇔ F) ∧ (+∞ = 1 ⇔ F) ∧ (1 ≤ −∞ ⇔ F) ∧ (1 < −∞ ⇔ F) ∧
(−∞ ≤ 1 ⇔ T) ∧ (−∞ < 1 ⇔ T) ∧ (1 = −∞ ⇔ F) ∧ (−∞ = 1 ⇔ F) ∧
(∀r. 1 ≤ Normal r ⇔ 1 ≤ r) ∧ (∀r. 1 < Normal r ⇔ 1 < r) ∧
(∀r. 1 = Normal r ⇔ r = 1) ∧ (∀r. Normal r ≤ 1 ⇔ r ≤ 1) ∧
(∀r. Normal r < 1 ⇔ r < 1) ∧ ∀r. Normal r = 1 ⇔ r = 1
[extreal_abs_def] Theorem
⊢ abs (Normal x) = Normal (abs x) ∧ abs −∞ = +∞ ∧ abs +∞ = +∞
[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_ainv_def] Theorem
⊢ -−∞ = +∞ ∧ -+∞ = −∞ ∧ ∀x. -Normal x = Normal (-x)
[extreal_cases] Theorem
⊢ ∀x. x = −∞ ∨ x = +∞ ∨ ∃r. x = Normal r
[extreal_dist_def] Theorem
⊢ extreal_dist (Normal x) (Normal y) =
dist (bounded_metric mr1) (x,y) ∧ extreal_dist +∞ +∞ = 0 ∧
extreal_dist −∞ −∞ = 0 ∧ extreal_dist −∞ +∞ = 1 ∧
extreal_dist −∞ (Normal v5) = 1 ∧ extreal_dist +∞ −∞ = 1 ∧
extreal_dist +∞ (Normal v7) = 1 ∧ extreal_dist (Normal v3) −∞ = 1 ∧
extreal_dist (Normal v3) +∞ = 1
[extreal_dist_ind] Theorem
⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ P +∞ +∞ ∧ P −∞ −∞ ∧ P −∞ +∞ ∧
(∀v5. P −∞ (Normal v5)) ∧ P +∞ −∞ ∧ (∀v7. P +∞ (Normal v7)) ∧
(∀v3. P (Normal v3) −∞) ∧ (∀v3. P (Normal v3) +∞) ⇒
∀v v1. P v v1
[extreal_dist_ismet] Theorem
⊢ ismet (UNCURRY extreal_dist)
[extreal_dist_normal] Theorem
⊢ ∀x y.
extreal_dist (Normal x) (Normal y) =
abs (x − y) / (1 + abs (x − y))
[extreal_distinct] Theorem
⊢ −∞ ≠ +∞ ∧ (∀a. −∞ ≠ Normal a) ∧ ∀a. +∞ ≠ Normal a
[extreal_div_def] Theorem
⊢ (∀r. Normal r / +∞ = Normal 0) ∧ (∀r. Normal r / −∞ = Normal 0) ∧
∀x r. r ≠ 0 ⇒ x / Normal r = x * (Normal r)⁻¹
[extreal_div_eq] Theorem
⊢ ∀x y. y ≠ 0 ⇒ Normal x / Normal y = Normal (x / y)
[extreal_double] Theorem
⊢ ∀x. x + x = 2 * x
[extreal_eq_zero] Theorem
⊢ ∀x. Normal x = 0 ⇔ x = 0
[extreal_inv_def] Theorem
⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹
[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_simps] Theorem
⊢ (∀x y. Normal x ≤ Normal y ⇔ x ≤ y) ∧ (∀x. −∞ ≤ x ⇔ T) ∧
(∀x. x ≤ +∞ ⇔ T) ∧ (∀x. Normal x ≤ −∞ ⇔ F) ∧
(∀x. +∞ ≤ Normal x ⇔ F) ∧ (+∞ ≤ −∞ ⇔ F)
[extreal_lim_sequentially_eq] Theorem
⊢ ∀f l.
(∃N. ∀n. N ≤ n ⇒ f n ≠ +∞ ∧ f n ≠ −∞) ∧ l ≠ +∞ ∧ l ≠ −∞ ⇒
((f --> l) sequentially ⇔ (real ∘ f --> real l) sequentially)
[extreal_lim_sequentially_eq'] Theorem
⊢ ∀f r.
(∃N. ∀n. N ≤ n ⇒ f n ≠ +∞ ∧ f n ≠ −∞) ⇒
((f --> Normal r) sequentially ⇔ (real ∘ f --> r) sequentially)
[extreal_lt_def] Theorem
⊢ ∀x y. x < y ⇔ ¬(y ≤ x)
[extreal_lt_eq] Theorem
⊢ ∀x y. Normal x < Normal y ⇔ x < y
[extreal_lt_simps] Theorem
⊢ (∀x y. Normal x < Normal y ⇔ x < y) ∧ (∀x. x < −∞ ⇔ F) ∧
(∀x. +∞ < x ⇔ F) ∧ (∀x. Normal x < +∞ ⇔ T) ∧
(∀x. −∞ < Normal x ⇔ T) ∧ (−∞ < +∞ ⇔ T)
[extreal_max_def] Theorem
⊢ ∀x y. max x y = if x ≤ y then y else x
[extreal_mean] Theorem
⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
[extreal_min_def] Theorem
⊢ ∀x y. min x y = if x ≤ y then x else y
[extreal_mr1_le_1] Theorem
⊢ ∀x y. dist extreal_mr1 (x,y) ≤ 1
[extreal_mr1_normal] Theorem
⊢ ∀x y.
dist extreal_mr1 (Normal x,Normal y) =
abs (x − y) / (1 + abs (x − y))
[extreal_mr1_thm] Theorem
⊢ dist extreal_mr1 = UNCURRY extreal_dist
[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_eq] Theorem
⊢ ∀x y. Normal x * Normal y = Normal (x * y)
[extreal_not_infty] Theorem
⊢ ∀x. Normal x ≠ −∞ ∧ Normal x ≠ +∞
[extreal_not_lt] Theorem
⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
[extreal_of_num_def] Theorem
⊢ ∀n. &n = Normal (&n)
[extreal_pow] Theorem
⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n
[extreal_pow_alt] Theorem
⊢ (∀x. x pow 0 = 1) ∧ ∀n x. x pow SUC n = x pow n * x
[extreal_pow_def] Theorem
⊢ (∀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_sqrt_def] Theorem
⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ sqrt +∞ = +∞
[extreal_sub] Theorem
⊢ ∀x y. x − y = x + -y
[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 x = +∞ ∧
−∞ − Normal x = −∞ ∧ Normal x − −∞ = +∞ ∧ Normal x − +∞ = −∞ ∧
−∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞
[extreal_sub_eq] Theorem
⊢ ∀x y. Normal x − Normal y = Normal (x − y)
[fn_minus] Theorem
⊢ ∀f x. f⁻ x = -min 0 (f x)
[fn_minus_abs] Theorem
⊢ ∀f. (abs ∘ f)⁻ = (λx. 0)
[fn_minus_mul_indicator] Theorem
⊢ ∀f s. (λx. f x * 𝟙 s x)⁻ = (λx. f⁻ x * 𝟙 s x)
[fn_plus] Theorem
⊢ ∀f x. f⁺ x = max 0 (f x)
[fn_plus_abs] Theorem
⊢ ∀f. (abs ∘ f)⁺ = abs ∘ f
[fn_plus_alt] Theorem
⊢ ∀f. f⁺ = (λx. if 0 ≤ f x then f x else 0)
[fn_plus_mul_indicator] Theorem
⊢ ∀f s. (λx. f x * 𝟙 s x)⁺ = (λx. f⁺ x * 𝟙 s x)
[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
[geometric_series_pow] Theorem
⊢ ∀x. 0 < x ∧ x < 1 ⇒ suminf (λn. x pow n) = (1 − x)⁻¹
[half_between] Theorem
⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
[half_cancel] Theorem
⊢ 2 * (1 / 2) = 1
[half_double] Theorem
⊢ ∀x. x / 2 + x / 2 = x
[half_not_infty] Theorem
⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞
[harmonic_series_pow_2] Theorem
⊢ suminf (λn. (&SUC n)² ⁻¹) < +∞
[indicator_fn_def] Theorem
⊢ ∀s. 𝟙 s = (λx. if x ∈ s then 1 else 0)
[indicator_fn_normal] Theorem
⊢ ∀s x. ∃r. 𝟙 s x = Normal r ∧ 0 ≤ r ∧ r ≤ 1
[indicator_fn_split] Theorem
⊢ ∀r s b.
FINITE r ∧ BIGUNION (IMAGE b r) = s ∧
(∀i j. i ∈ r ∧ j ∈ r ∧ i ≠ j ⇒ DISJOINT (b i) (b j)) ⇒
∀a. a ⊆ s ⇒ 𝟙 a = (λx. ∑ (λi. 𝟙 (a ∩ b i) x) r)
[indicator_fn_suminf] Theorem
⊢ ∀a x.
(∀m n. m ≠ n ⇒ DISJOINT (a m) (a n)) ⇒
suminf (λi. 𝟙 (a i) x) = 𝟙 (BIGUNION (IMAGE a 𝕌(:num))) x
[ineq_imp] Theorem
⊢ (∀x y. x < y ⇒ ¬(y < x)) ∧ (∀x y. x < y ⇒ x ≠ y) ∧
(∀x y. x < y ⇒ ¬(y ≤ x)) ∧ (∀x y. x < y ⇒ x ≤ y) ∧
∀x y. x ≤ y ⇒ ¬(y < x)
[inf_cminus] Theorem
⊢ ∀f c.
Normal c − inf (IMAGE f 𝕌(:α)) =
sup (IMAGE (λn. Normal c − f n) 𝕌(:α))
[inf_cmul] Theorem
⊢ ∀P r.
0 < r ⇒
inf {x * Normal r | 0 < x ∧ P x} =
Normal r * inf {x | 0 < x ∧ P x}
[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] Theorem
⊢ ∀p q.
(∀n. p n ≤ q n) ⇒ inf (IMAGE p 𝕌(:num)) ≤ inf (IMAGE q 𝕌(:num))
[inf_mono_subset] Theorem
⊢ ∀p q. p ⊆ q ⇒ inf q ≤ inf p
[inf_num] Theorem
⊢ inf (λx. ∃n. x = -&n) = −∞
[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 = −∞
[infty_pow2] Theorem
⊢ +∞ ² = +∞ ∧ −∞ ² = +∞
[infty_powr] Theorem
⊢ ∀a. 0 < a ⇒ +∞ powr a = +∞
[inv_1over] Theorem
⊢ ∀x. x ≠ 0 ⇒ x⁻¹ = 1 / x
[inv_infty] Theorem
⊢ +∞ ⁻¹ = 0 ∧ −∞ ⁻¹ = 0
[inv_inj] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)
[inv_inv] Theorem
⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ ⁻¹ = x
[inv_le_antimono] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)
[inv_le_antimono_imp] Theorem
⊢ ∀x y. 0 < y ∧ y ≤ x ⇒ x⁻¹ ≤ y⁻¹
[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)
[inv_powr] Theorem
⊢ ∀x p. 0 < x ∧ 0 < p ∧ p ≠ +∞ ⇒ x⁻¹ powr p = (x powr p)⁻¹
[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] Theorem
⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y ≤ x + y ⇔ 0 ≤ x)
[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] Theorem
⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y ≤ x * z ⇔ y ≤ 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_mul2] Theorem
⊢ ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2
[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_negl] Theorem
⊢ ∀x y. -x ≤ y ⇔ -y ≤ x
[le_negr] Theorem
⊢ ∀x y. x ≤ -y ⇔ y ≤ -x
[le_not_infty] Theorem
⊢ (∀x. 0 ≤ x ⇒ 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] Theorem
⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z ≤ y * z ⇔ x ≤ y)
[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
[leeq_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
[lim_sequentially_imp_extreal_lim] Theorem
⊢ ∀f l.
(f --> l) sequentially ⇒ (Normal ∘ f --> Normal l) sequentially
[linv_uniq] Theorem
⊢ ∀x y. x * y = 1 ⇒ x = y⁻¹
[ln_1] Theorem
⊢ ln 1 = 0
[ln_inv] Theorem
⊢ ∀x. 0 < x ⇒ ln x⁻¹ = -ln x
[ln_mul] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ ln (x * y) = ln x + ln y
[ln_neg] Theorem
⊢ ∀x. 0 ≤ x ∧ x ≤ 1 ⇒ ln x ≤ 0
[ln_neg_lt] Theorem
⊢ ∀x. 0 ≤ x ∧ x < 1 ⇒ ln x < 0
[ln_not_neginf] Theorem
⊢ ∀x. 0 < x ⇒ ln x ≠ −∞
[ln_pos] Theorem
⊢ ∀x. 1 ≤ x ⇒ 0 ≤ ln x
[ln_pos_lt] Theorem
⊢ ∀x. 1 < x ⇒ 0 < ln x
[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] Theorem
⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x < x + y ⇔ 0 < y)
[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'] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. x ∈ P ∧ x ≠ +∞) ∧ inf P ≠ −∞ ⇒
∃x. x ∈ P ∧ 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. −∞ < Normal x ∧ Normal x < +∞) ∧
(∀x. ¬(x < −∞) ∧ ¬(+∞ < x)) ∧ (∀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_lmul_imp] Theorem
⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ∧ y < z ⇒ x * y < x * z
[lt_lsub_imp] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ∧ y < z ⇒ x − z < x − y
[lt_max] Theorem
⊢ ∀x y z. x < max y z ⇔ x < y ∨ x < z
[lt_max_between] Theorem
⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
[lt_max_fn_seq] Theorem
⊢ ∀f x y n. x < max_fn_seq f n y ⇔ ∃i. i ≤ n ∧ x < f i y
[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_rmul_imp] Theorem
⊢ ∀x y z. x < y ∧ 0 < z ∧ z ≠ +∞ ⇒ x * z < y * z
[lt_rsub_imp] Theorem
⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ∧ x < y ⇒ x − z < y − z
[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_0] Theorem
⊢ ∀g. max_fn_seq g 0 = g 0
[max_fn_seq_alt_sup] Theorem
⊢ ∀f x n. max_fn_seq f n x = sup (IMAGE (λi. f i x) (count (SUC n)))
[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_cong] Theorem
⊢ ∀f g x.
(∀n. f n x = g n x) ⇒ ∀n. max_fn_seq f n x = max_fn_seq g n x
[max_fn_seq_le] Theorem
⊢ ∀f x y n. max_fn_seq f n x ≤ y ⇔ ∀i. i ≤ n ⇒ f i x ≤ y
[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
[monoidal_mul] Theorem
⊢ monoidal $*
[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. r ≠ 0 ⇒ x = x * Normal r / Normal r
[mul_infty] Theorem
⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞
[mul_infty'] Theorem
⊢ ∀x. x < 0 ⇒ +∞ * 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_powr] Theorem
⊢ ∀x y a.
0 ≤ x ∧ 0 ≤ y ∧ 0 < a ∧ a ≠ +∞ ⇒
(x * y) powr a = x powr a * y powr a
[mul_rcancel] Theorem
⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (y * x = z * x ⇔ x = 0 ∨ y = z)
[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
[neutral_mul] Theorem
⊢ neutral $* = 1
[nonneg_abs] Theorem
⊢ ∀f. nonneg (abs ∘ f)
[nonneg_fn_abs] Theorem
⊢ ∀f. nonneg f ⇒ abs ∘ f = f
[nonneg_fn_minus] Theorem
⊢ ∀f. nonneg f ⇒ f⁻ = (λx. 0)
[nonneg_fn_plus] Theorem
⊢ ∀f. nonneg f ⇒ f⁺ = f
[normal_0] Theorem
⊢ Normal 0 = 0
[normal_1] Theorem
⊢ Normal 1 = 1
[normal_exp] Theorem
⊢ ∀r. exp (Normal r) = Normal (exp r)
[normal_inv_eq] Theorem
⊢ ∀x. x ≠ 0 ⇒ Normal x⁻¹ = (Normal x)⁻¹
[normal_minus1] Theorem
⊢ Normal (-1) = -1
[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
[one_powr] Theorem
⊢ ∀a. 0 ≤ a ⇒ 1 powr a = 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_2_abs] Theorem
⊢ ∀x. x² = abs x * abs x
[pow_add] Theorem
⊢ ∀x n m. x pow (n + m) = x pow n * x pow m
[pow_ainv_even] Theorem
⊢ ∀n. EVEN n ⇒ ∀x. -x pow n = x pow n
[pow_ainv_odd] Theorem
⊢ ∀n. ODD n ⇒ ∀x. -x pow n = -(x pow n)
[pow_div] Theorem
⊢ ∀n x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ (x / y) pow n = x pow n / y pow n
[pow_eq] Theorem
⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x = y ⇔ x pow n = y pow n)
[pow_even_le] Theorem
⊢ ∀n. EVEN n ⇒ ∀x. 0 ≤ x pow n
[pow_half_pos_le] Theorem
⊢ ∀n. 0 ≤ (1 / 2) pow n
[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
⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ x pow n
[pow_pos_lt] Theorem
⊢ ∀n x. 0 < x ⇒ 0 < x pow n
[pow_pow] Theorem
⊢ ∀x m n. (x pow m) pow n = x pow (m * 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_1] Theorem
⊢ ∀x. 0 ≤ x ⇒ x powr 1 = x
[powr_add] Theorem
⊢ ∀a b c.
0 ≤ a ∧ 0 ≤ b ∧ b ≠ +∞ ∧ 0 ≤ c ∧ c ≠ +∞ ⇒
a powr (b + c) = a powr b * a powr c
[powr_eq_0] Theorem
⊢ ∀x a. 0 ≤ x ∧ 0 < a ∧ a ≠ +∞ ⇒ (x powr a = 0 ⇔ x = 0)
[powr_ge_1] Theorem
⊢ ∀a p. 1 ≤ a ∧ 0 ≤ p ⇒ 1 ≤ a powr p
[powr_infty] Theorem
⊢ ∀x. (1 < x ⇒ x powr +∞ = +∞) ∧ (x = 1 ⇒ x powr +∞ = 1) ∧
(0 ≤ x ∧ x < 1 ⇒ x powr +∞ = 0)
[powr_le_eq] Theorem
⊢ ∀a b c.
1 < a ∧ a ≠ +∞ ∧ 0 ≤ b ∧ 0 ≤ c ⇒ (a powr b ≤ a powr c ⇔ b ≤ c)
[powr_mono_eq] Theorem
⊢ ∀a b c.
0 ≤ a ∧ 0 ≤ c ∧ 0 < b ∧ b ≠ +∞ ⇒ (a powr b ≤ c powr b ⇔ a ≤ c)
[powr_pos] Theorem
⊢ ∀x a. 0 ≤ x powr a
[powr_pos_lt] Theorem
⊢ ∀x a. 0 < x ∧ 0 ≤ a ∧ a ≠ +∞ ⇒ 0 < x powr a
[powr_powr] Theorem
⊢ ∀a b c.
0 ≤ a ∧ 0 < b ∧ 0 < c ∧ b ≠ +∞ ∧ c ≠ +∞ ⇒
(a powr b) powr c = a powr (b * c)
[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_0] Theorem
⊢ real 0 = 0
[real_def] Theorem
⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r
[real_normal] Theorem
⊢ ∀x. real (Normal x) = x
[rinv_uniq] Theorem
⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹
[sqrt_0] Theorem
⊢ sqrt 0 = 0
[sqrt_1] Theorem
⊢ sqrt 1 = 1
[sqrt_le_n] Theorem
⊢ ∀n. sqrt (&n) ≤ &n
[sqrt_le_x] Theorem
⊢ ∀x. 1 ≤ x ⇒ sqrt x ≤ x
[sqrt_mono_le] Theorem
⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
[sqrt_mul] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (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_pos_ne] Theorem
⊢ ∀x. 0 < x ⇒ sqrt x ≠ 0
[sqrt_pow2] Theorem
⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x
[sqrt_powr] Theorem
⊢ ∀x. 0 ≤ x ⇒ sqrt x = x powr 2⁻¹
[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_add_normal] Theorem
⊢ ∀x r. x − Normal r + Normal r = x
[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_sub_imp] Theorem
⊢ ∀w x y z. w ≤ x ∧ z ≤ y ⇒ w − 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
⊢ ∀x y. x − -y = x + y
[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_insert] Theorem
⊢ ∀x s. sup (x INSERT s) = if s = ∅ then x else max x (sup s)
[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_epsilon'] Theorem
⊢ ∀P e.
0 < e ∧ (∃x. x ∈ P ∧ x ≠ −∞) ∧ sup P ≠ +∞ ⇒
∃x. x ∈ P ∧ 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
[x_half_half] Theorem
⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x
[young_inequality] Theorem
⊢ ∀a b p q.
0 ≤ a ∧ 0 ≤ b ∧ 0 < p ∧ 0 < q ∧ p ≠ +∞ ∧ q ≠ +∞ ∧ p⁻¹ + q⁻¹ = 1 ⇒
a * b ≤ a powr p / p + b powr q / q
[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
HOL 4, Trindemossen-1