100thms_12.mg

Name Size Modified
.. — —
BezoutThm.html 11 KB
DescrR_i_io_12.html 5 KB
Descr_Vo1_prop.html 3 KB
Descr_ii_prop.html 5 KB
Descr_iii_prop.html 7 KB
EmptyE.html 729 bytes
Empty_In_Power.html 668 bytes
Empty_Subq_eq.html 1 KB
Empty_eq.html 1 KB
Eps_i_ex.html 940 bytes
Euclid_lemma.html 37 KB
Euclid_lemma_Pi_SNo.html 12 KB
FalseE.html 229 bytes
If_i_0.html 4 KB
If_i_1.html 4 KB
If_i_correct.html 5 KB
If_i_or.html 2 KB
If_ii_0.html 1 KB
If_ii_1.html 1 KB
If_iii_0.html 2 KB
If_iii_1.html 2 KB
In_0_1.html 331 bytes
In_0_2.html 519 bytes
In_1_2.html 331 bytes
In_irref.html 1 KB
In_no2cycle.html 2 KB
In_rec_G_ii_In_rec_ii.html 3 KB
In_rec_G_ii_In_rec_ii_d.html 2 KB
In_rec_G_ii_c.html 4 KB
In_rec_G_ii_f.html 11 KB
In_rec_G_ii_inv.html 10 KB
In_rec_G_iii_In_rec_iii.html 3 KB
In_rec_G_iii_In_rec_iii_d.html 2 KB
In_rec_G_iii_c.html 5 KB
In_rec_G_iii_f.html 12 KB
In_rec_G_iii_inv.html 10 KB
In_rec_i_G_In_rec_i.html 3 KB
In_rec_i_G_In_rec_i_d.html 2 KB
In_rec_i_G_c.html 4 KB
In_rec_i_G_f.html 11 KB
In_rec_i_G_inv.html 9 KB
In_rec_i_eq.html 1 KB
In_rec_ii_eq.html 1 KB
In_rec_iii_eq.html 1 KB
Inj0E.html 549 bytes
Inj0I.html 549 bytes
Inj0_0.html 351 bytes
Inj0_Inj1_neq.html 4 KB
Inj0_inj.html 1 KB
Inj0_pair_0_eq.html 1 KB
Inj0_setsum.html 2 KB
Inj0_setsum_0L.html 9 KB
Inj1E.html 5 KB
Inj1I1.html 1 KB
Inj1I2.html 2 KB
Inj1NE1.html 1 KB
Inj1NE2.html 1 KB
Inj1_eq.html 5 KB
Inj1_inj.html 1 KB
Inj1_pair_1_eq.html 1 KB
Inj1_setsum.html 2 KB
Inj1_setsum_1L.html 15 KB
KnasterTarski_set.html 13 KB
PNoEqLe_tra.html 5 KB
PNoEqLt_tra.html 19 KB
PNoEq_PSNo.html 11 KB
PNoEq_antimon.html 2 KB
PNoEq_ref.html 422 bytes
PNoEq_rel_strict_imv.html 2 KB
PNoEq_rel_strict_lowerbd.html 5 KB
PNoEq_rel_strict_upperbd.html 5 KB
PNoEq_strict_imv.html 2 KB
PNoEq_strict_lowerbd.html 4 KB
PNoEq_strict_upperbd.html 4 KB
PNoEq_sym.html 943 bytes
PNoEq_tra.html 1 KB
PNoLeI1.html 1 KB
PNoLeI2.html 1 KB
PNoLeLt_tra.html 6 KB
PNoLe_antisym.html 14 KB
PNoLe_downc.html 6 KB
PNoLe_ref.html 515 bytes
PNoLe_tra.html 7 KB
PNoLe_upc.html 6 KB
PNoLtE.html 2 KB
PNoLtEq_tra.html 19 KB
PNoLtI1.html 2 KB
PNoLtI2.html 3 KB
PNoLtI3.html 3 KB
PNoLtLe_tra.html 6 KB
PNoLt_E.html 2 KB
PNoLt_SNoLt_PSNo.html 9 KB
PNoLt_irref.html 1 KB
PNoLt_irref__2.html 3 KB
PNoLt_mon.html 3 KB
PNoLt_pwise_downc_upc.html 16 KB
PNoLt_tra.html 116 KB
PNoLt_trichotomy_or.html 26 KB
PNoLt_trichotomy_or__2.html 21 KB
PNo_bd_In.html 9 KB
PNo_bd_pred.html 1 KB
PNo_bd_pred_lem.html 1 KB
PNo_downc_ref.html 2 KB
PNo_extend0_eq.html 4 KB
PNo_extend1_eq.html 4 KB
PNo_lenbdd_least_rep2_exuniq2.html 31 KB
PNo_lenbdd_strict_imv_ex.html 6 KB
PNo_lenbdd_strict_imv_extend0.html 50 KB
PNo_lenbdd_strict_imv_extend1.html 52 KB
PNo_lenbdd_strict_imv_split.html 4 KB
PNo_rel_imv_bdd_ex.html 9 KB
PNo_rel_imv_ex.html 415 KB
PNo_rel_split_imv_imp_strict_imv.html 82 KB
PNo_rel_strict_imv_antimon.html 3 KB
PNo_rel_strict_lowerbd_antimon.html 14 KB
PNo_rel_strict_upperbd_antimon.html 13 KB
PNo_strict_imv_imp_rel_strict_imv.html 5 KB
PNo_strict_imv_pred_eq.html 37 KB
PNo_strict_lowerbd_imp_rel_strict_lowerbd.html 27 KB
PNo_strict_upperbd_imp_rel_strict_upperbd.html 28 KB
PNo_upc_ref.html 2 KB
PiI.html 11 KB
Pi_SNo_0.html 677 bytes
Pi_SNo_In_int.html 7 KB
Pi_SNo_In_omega.html 6 KB
Pi_SNo_S.html 1 KB
Pi_SNo_divides.html 13 KB
Pi_SNo_eq.html 7 KB
Pi_nat_0.html 677 bytes
Pi_nat_0_inv.html 14 KB
Pi_nat_S.html 1 KB
Pi_nat_divides.html 14 KB
Pi_nat_p.html 6 KB
PigeonHole_nat.html 57 KB
Pigeonhole_not_atleastp_ordsucc.html 1 KB
PowerE.html 648 bytes
PowerI.html 648 bytes
Power_0_Sing_0.html 4 KB
ReplE.html 705 bytes
ReplE__2.html 2 KB
ReplE_impred.html 1 KB
ReplEq_ext.html 2 KB
ReplEq_ext_sub.html 4 KB
ReplEq_setprod_ext.html 5 KB
ReplI.html 2 KB
ReplSepE.html 4 KB
ReplSepE_impred.html 2 KB
ReplSepI.html 1 KB
Repl_Empty.html 2 KB
Repl_finite.html 17 KB
Repl_inv_eq.html 7 KB
Repl_invol_eq.html 658 bytes
SNoCutP_0_0.html 887 bytes
SNoCutP_L_0.html 3 KB
SNoCutP_SNoCut.html 157 KB
SNoCutP_SNoCut_L.html 1 KB
SNoCutP_SNoCut_R.html 1 KB
SNoCutP_SNoCut_fst.html 1 KB
SNoCutP_SNoCut_impred.html 1 KB
SNoCutP_SNoCut_lim.html 28 KB
SNoCutP_SNoCut_omega.html 575 bytes
SNoCutP_SNoL_SNoR.html 18 KB
SNoCutP_SNo_SNoCut.html 1 KB
SNoCut_0_0.html 9 KB
SNoCut_Le.html 50 KB
SNoCut_ext.html 7 KB
SNoElts_mon.html 7 KB
SNoEq_I.html 384 bytes
SNoEq_sym.html 913 bytes
SNoEq_tra.html 1 KB
SNoL_0.html 3 KB
SNoL_1.html 12 KB
SNoL_E.html 5 KB
SNoL_I.html 2 KB
SNoL_SNoCutP_ex.html 14 KB
SNoL_SNoS.html 851 bytes
SNoL_SNoS__2.html 2 KB
SNoL_minus_SNoR.html 14 KB
SNoL_nonneg_0.html 1 KB
SNoL_nonneg_1.html 4 KB
SNoL_or_SNoR_impred.html 4 KB
SNoLeE.html 5 KB
SNoLeLt_tra.html 2 KB
SNoLe_antisym.html 3 KB
SNoLe_ref.html 770 bytes
SNoLe_tra.html 2 KB
SNoLev.html 789 bytes
SNoLev_0.html 431 bytes
SNoLev_0_eq_0.html 3 KB
SNoLev_In_real_SNoS_omega.html 5 KB
SNoLev_PSNo.html 6 KB
SNoLev_eps.html 2 KB
SNoLev_ind.html 6 KB
SNoLev_ind2.html 18 KB
SNoLev_ind3.html 40 KB
SNoLev_ordinal.html 789 bytes
SNoLev_prop.html 1 KB
SNoLev_uniq.html 1 KB
SNoLev_uniq2.html 2 KB
SNoLev_uniq_Subq.html 12 KB
SNoLtE.html 40 KB
SNoLtI2.html 1 KB
SNoLtI3.html 1 KB
SNoLtLe.html 1 KB
SNoLtLe_or.html 3 KB
SNoLtLe_tra.html 2 KB
SNoLt_0_1.html 953 bytes
SNoLt_0_2.html 953 bytes
SNoLt_1_2.html 953 bytes
SNoLt_PSNo_PNoLt.html 9 KB
SNoLt_SNoL_or_SNoR_impred.html 5 KB
SNoLt_irref.html 774 bytes
SNoLt_minus_pos.html 1 KB
SNoLt_tra.html 3 KB
SNoLt_trichotomy_or.html 5 KB
SNoLt_trichotomy_or_impred.html 1 KB
SNoR_0.html 3 KB
SNoR_1.html 642 bytes
SNoR_E.html 5 KB
SNoR_I.html 2 KB
SNoR_SNoCutP_ex.html 14 KB
SNoR_SNoS.html 851 bytes
SNoR_SNoS__2.html 2 KB
SNoS_E.html 2 KB
SNoS_E2.html 6 KB
SNoS_I.html 7 KB
SNoS_I2.html 1 KB
SNoS_In_neq.html 5 KB
SNoS_SNoLev.html 3 KB
SNoS_Subq.html 2 KB
SNoS_finite.html 22 KB
SNoS_omega_Lev_equip.html 207 KB
SNoS_omega_SNoL_finite.html 6 KB
SNoS_omega_SNoL_max_exists.html 4 KB
SNoS_omega_SNoR_finite.html 6 KB
SNoS_omega_SNoR_min_exists.html 4 KB
SNoS_omega_diadic_rational_p.html 4 KB
SNoS_omega_diadic_rational_p_lem.html 71 KB
SNoS_omega_drat_intvl.html 18 KB
SNoS_omega_real.html 44 KB
SNoS_ordsucc_omega_bdd_above.html 19 KB
SNoS_ordsucc_omega_bdd_below.html 6 KB
SNoS_ordsucc_omega_bdd_drat_intvl.html 61 KB
SNoS_ordsucc_omega_bdd_eps_pos.html 24 KB
SNo_0.html 425 bytes
SNo_1.html 623 bytes
SNo_2.html 623 bytes
SNo_PSNo.html 36 KB
SNo_PSNo_eta.html 25 KB
SNo_PSNo_eta__2.html 2 KB
SNo_SNo.html 1 KB
SNo_Subq.html 16 KB
SNo__eps.html 45 KB
SNo_abs_SNo.html 2 KB
SNo_add_SNo.html 2 KB
SNo_add_SNo_3.html 1 KB
SNo_add_SNo_3c.html 1 KB
SNo_add_SNo_4.html 1 KB
SNo_approx_real.html 98 KB
SNo_approx_real_lem.html 33 KB
SNo_approx_real_rep.html 81 KB
SNo_div_SNo.html 1 KB
SNo_eps.html 2 KB
SNo_eps_1.html 630 bytes
SNo_eps_SNoS_omega.html 2 KB
SNo_eps_decr.html 16 KB
SNo_eps_pos.html 6 KB
SNo_eq.html 5 KB
SNo_eta.html 36 KB
SNo_etaE.html 38 KB
SNo_exp_SNo_nat.html 3 KB
SNo_extend0_SNo.html 2 KB
SNo_extend0_SNoEq.html 9 KB
SNo_extend0_SNoLev.html 1 KB
SNo_extend0_SNo__2.html 1 KB
SNo_extend0_nIn.html 9 KB
SNo_extend0_restr_eq.html 9 KB
SNo_extend1_In.html 3 KB
SNo_extend1_SNo.html 2 KB
SNo_extend1_SNoEq.html 9 KB
SNo_extend1_SNoLev.html 1 KB
SNo_extend1_SNo__2.html 1 KB
SNo_extend1_restr_eq.html 9 KB
SNo_foil.html 12 KB
SNo_foil_mm.html 5 KB
SNo_ind.html 15 KB
SNo_max_SNoLev.html 17 KB
SNo_max_ordinal.html 2 KB
SNo_minus_SNo.html 1 KB
SNo_mul_SNo.html 921 bytes
SNo_mul_SNo_3.html 1 KB
SNo_mul_SNo_lem.html 2 KB
SNo_nonneg_sqr_uniq.html 9 KB
SNo_omega.html 442 bytes
SNo_ordinal_ind.html 3 KB
SNo_ordinal_ind2.html 7 KB
SNo_ordinal_ind3.html 11 KB
SNo_pos_eps_Le.html 22 KB
SNo_pos_eps_Lt.html 21 KB
SNo_pos_sqr_uniq.html 6 KB
SNo_prereal_decr_upper_approx.html 26 KB
SNo_prereal_incr_lower_approx.html 109 KB
SNo_prereal_incr_lower_pos.html 31 KB
SNo_rec2_G_prop.html 14 KB
SNo_rec2_eq.html 59 KB
SNo_rec2_eq_1.html 4 KB
SNo_rec_i_eq.html 50 KB
SNo_rec_ii_eq.html 51 KB
SNo_recip_SNo.html 6 KB
SNo_recip_SNo_pos.html 869 bytes
SNo_recip_lem1.html 18 KB
SNo_recip_lem2.html 18 KB
SNo_recip_lem3.html 18 KB
SNo_recip_lem4.html 18 KB
SNo_recip_pos_pos.html 6 KB
SNo_recipaux_0.html 3 KB
SNo_recipaux_S.html 3 KB
SNo_recipaux_ext.html 48 KB
SNo_recipaux_lem1.html 148 KB
SNo_recipaux_lem2.html 24 KB
SNo_recipauxset_E.html 5 KB
SNo_recipauxset_I.html 6 KB
SNo_recipauxset_ext.html 5 KB
SNo_sqrt_SNo_SNoCutP.html 1 KB
SNo_sqrt_SNo_nonneg.html 1 KB
SNo_sqrtaux_0.html 3 KB
SNo_sqrtaux_0_1_prop.html 2 KB
SNo_sqrtaux_0_prop.html 1 KB
SNo_sqrtaux_1_prop.html 1 KB
SNo_sqrtaux_S.html 3 KB
SNo_sqrtaux_ext.html 15 KB
SNo_sqrtaux_mon.html 3 KB
SNo_sqrtaux_mon_lem.html 31 KB
SNo_sqrtauxset_0.html 1 KB
SNo_sqrtauxset_0__2.html 2 KB
SNo_sqrtauxset_E.html 5 KB
SNo_sqrtauxset_I.html 6 KB
SNo_sqrtauxset_real.html 10 KB
SNo_sqrtauxset_real_nonneg.html 30 KB
SNo_zero_or_sqr_pos.html 4 KB
SchroederBernstein.html 69 KB
Self_In_Power.html 617 bytes
SepE.html 18 KB
SepE1.html 801 bytes
SepE2.html 768 bytes
SepI.html 9 KB
Sep_Empty.html 1 KB
Sep_In_Power.html 826 bytes
Sep_Subq.html 211 bytes
Sigma_E.html 6 KB
Sigma_eta_proj0_proj1.html 11 KB
SingE.html 917 bytes
SingI.html 425 bytes
Sing_finite.html 1 KB
Subq_1_Sing0.html 2 KB
Subq_2_UPair01.html 4 KB
Subq_Empty.html 770 bytes
Subq_SNoS_omega_rational.html 18 KB
Subq_Sing0_1.html 1023 bytes
Subq_atleastp.html 2 KB
Subq_binunion_eq.html 4 KB
Subq_finite.html 18 KB
Subq_int_SNoS_omega.html 1 KB
Subq_omega_int.html 1 KB
Subq_rational_real.html 1 KB
Subq_ref.html 388 bytes
Subq_tra.html 962 bytes
TransSet_In_ordsucc_Subq.html 1 KB
TransSet_ordsucc.html 4 KB
TransSet_ordsucc_In_Subq.html 3 KB
UPairE.html 8 KB
UPairI1.html 6 KB
UPairI2.html 5 KB
UnionE.html 1 KB
UnionE_impred.html 1 KB
UnionI.html 2 KB
Union_ordsucc_eq.html 6 KB
Unj_Inj0_eq.html 16 KB
Unj_Inj1_eq.html 18 KB
Unj_eq.html 6 KB
ZF_Power_closed.html 897 bytes
ZF_Repl_closed.html 1 KB
ZF_Sing_closed.html 638 bytes
ZF_UPair_closed.html 35 KB
ZF_Union_closed.html 896 bytes
ZF_binunion_closed.html 1 KB
ZF_closed_E.html 767 bytes
ZF_ordsucc_closed.html 1 KB
abs_SNo_dist_swap.html 6 KB
abs_SNo_minus.html 11 KB
add_SNo_0L.html 28 KB
add_SNo_0R.html 1 KB
add_SNo_1_1_2.html 1 KB
add_SNo_1_ordsucc.html 2 KB
add_SNo_3_2_3_Lt1.html 2 KB
add_SNo_3_3_3_Lt1.html 3 KB
add_SNo_3a_2b.html 6 KB
add_SNo_In_omega.html 2 KB
add_SNo_Le1.html 3 KB
add_SNo_Le1_cancel.html 5 KB
add_SNo_Le2.html 3 KB
add_SNo_Le3.html 5 KB
add_SNo_Lev_bd.html 163 KB
add_SNo_Lt1.html 20 KB
add_SNo_Lt1_cancel.html 5 KB
add_SNo_Lt2.html 20 KB
add_SNo_Lt2_cancel.html 1 KB
add_SNo_Lt3.html 3 KB
add_SNo_Lt3a.html 5 KB
add_SNo_Lt3b.html 5 KB
add_SNo_Lt4.html 3 KB
add_SNo_Lt_subprop2.html 12 KB
add_SNo_Lt_subprop3a.html 9 KB
add_SNo_Lt_subprop3b.html 6 KB
add_SNo_Lt_subprop3c.html 14 KB
add_SNo_Lt_subprop3d.html 27 KB
add_SNo_SNoCutP.html 1 KB
add_SNo_SNoL_interpolate.html 57 KB
add_SNo_SNoR_interpolate.html 57 KB
add_SNo_SNoS_omega.html 13 KB
add_SNo_assoc.html 182 KB
add_SNo_assoc_4.html 3 KB
add_SNo_cancel_L.html 3 KB
add_SNo_cancel_R.html 3 KB
add_SNo_com.html 39 KB
add_SNo_com_3_0_1.html 1 KB
add_SNo_com_3b_1_2.html 1 KB
add_SNo_com_4_inner_mid.html 4 KB
add_SNo_diadic_rational_p.html 37 KB
add_SNo_eps_Lt.html 2 KB
add_SNo_eps_Lt__2.html 2 KB
add_SNo_eq.html 26 KB
add_SNo_minus_L2.html 3 KB
add_SNo_minus_L2__2.html 1 KB
add_SNo_minus_Le12b3.html 10 KB
add_SNo_minus_Le1b.html 3 KB
add_SNo_minus_Le1b3.html 3 KB
add_SNo_minus_Le2.html 4 KB
add_SNo_minus_Le2b.html 3 KB
add_SNo_minus_Lt1.html 3 KB
add_SNo_minus_Lt12b3.html 10 KB
add_SNo_minus_Lt1b.html 3 KB
add_SNo_minus_Lt1b3.html 3 KB
add_SNo_minus_Lt2.html 4 KB
add_SNo_minus_Lt2b.html 3 KB
add_SNo_minus_Lt2b3.html 3 KB
add_SNo_minus_Lt_lem.html 14 KB
add_SNo_minus_R2.html 2 KB
add_SNo_minus_R2__2.html 1 KB
add_SNo_minus_SNo_linv.html 62 KB
add_SNo_minus_SNo_prop2.html 2 KB
add_SNo_minus_SNo_prop3.html 5 KB
add_SNo_minus_SNo_prop5.html 3 KB
add_SNo_minus_SNo_rinv.html 2 KB
add_SNo_omega_In_cases.html 12 KB
add_SNo_ordinal_InL.html 6 KB
add_SNo_ordinal_InR.html 5 KB
add_SNo_ordinal_SL.html 73 KB
add_SNo_ordinal_SNoCutP.html 14 KB
add_SNo_ordinal_SR.html 7 KB
add_SNo_ordinal_eq.html 13 KB
add_SNo_ordinal_ordinal.html 27 KB
add_SNo_prop1.html 171 KB
add_SNo_rotate_3_1.html 3 KB
add_SNo_rotate_4_1.html 2 KB
add_SNo_rotate_5_1.html 2 KB
add_SNo_rotate_5_2.html 2 KB
add_nat_0L.html 3 KB
add_nat_0R.html 645 bytes
add_nat_1_1_2.html 2 KB
add_nat_In_L.html 2 KB
add_nat_In_R.html 6 KB
add_nat_SL.html 6 KB
add_nat_SR.html 865 bytes
add_nat_Subq_L.html 2 KB
add_nat_Subq_R.html 6 KB
add_nat_Subq_R__2.html 4 KB
add_nat_add_SNo.html 10 KB
add_nat_asso.html 7 KB
add_nat_cancel_R.html 6 KB
add_nat_com.html 5 KB
add_nat_p.html 4 KB
adjoin_finite.html 33 KB
and3E.html 765 bytes
and3I.html 926 bytes
and4I.html 961 bytes
and5I.html 1 KB
and6I.html 1 KB
and7I.html 1 KB
andEL.html 412 bytes
andER.html 412 bytes
andI.html 351 bytes
ap0_Sigma.html 550 bytes
ap1_Sigma.html 780 bytes
apE.html 6 KB
apI.html 4 KB
ap_Pi.html 1 KB
atleastp_SNoS_ordsucc_omega_Power_omega.html 77 KB
atleastp_antisym_equip.html 2 KB
atleastp_omega_infinite.html 7 KB
atleastp_tra.html 3 KB
beta.html 5 KB
bijE.html 1 KB
bijI.html 2 KB
bij_comp.html 11 KB
bij_id.html 2 KB
bij_inj.html 627 bytes
bij_inv.html 12 KB
bij_surj.html 2 KB
binintersectE.html 693 bytes
binintersectE1.html 695 bytes
binintersectE2.html 695 bytes
binintersectI.html 753 bytes
binintersect_Subq_1.html 229 bytes
binintersect_Subq_2.html 229 bytes
binintersect_Subq_eq_1.html 1 KB
binintersect_Subq_max.html 2 KB
binintersect_com.html 1 KB
binintersect_com_Subq.html 1 KB
binunionE.html 4 KB
binunionE__2.html 1 KB
binunionI1.html 2 KB
binunionI2.html 2 KB
binunion_Subq_1.html 221 bytes
binunion_Subq_2.html 221 bytes
binunion_Subq_min.html 2 KB
binunion_asso.html 9 KB
binunion_com.html 1 KB
binunion_com_Subq.html 2 KB
binunion_finite.html 3 KB
binunion_idl.html 3 KB
binunion_idr.html 835 bytes
binunion_remove1_eq.html 7 KB
cases_1.html 2 KB
cases_2.html 2 KB
diadic_rational_p_SNoS_omega.html 9 KB
div_SNo_0_denum.html 1 KB
div_SNo_0_num.html 888 bytes
div_SNo_neg_pos.html 2 KB
div_SNo_pos_LtL.html 8 KB
div_SNo_pos_LtL__2.html 6 KB
div_SNo_pos_LtR.html 8 KB
div_SNo_pos_LtR__2.html 6 KB
div_SNo_pos_pos.html 2 KB
div_div_SNo.html 20 KB
div_mul_SNo_invL.html 1 KB
divides_int_0.html 4 KB
divides_int_1.html 3 KB
divides_int_add_SNo.html 10 KB
divides_int_div_SNo_int.html 10 KB
divides_int_divides_nat.html 17 KB
divides_int_minus_SNo.html 6 KB
divides_int_mul_SNo.html 11 KB
divides_int_mul_SNo_L.html 8 KB
divides_int_mul_SNo_R.html 3 KB
divides_int_pos_Le.html 27 KB
divides_int_prime_nat_eq.html 6 KB
divides_int_ref.html 3 KB
divides_nat_divides_int.html 6 KB
divides_nat_mulL.html 2 KB
divides_nat_mulR.html 3 KB
divides_nat_mul_SNo_L.html 2 KB
divides_nat_mul_SNo_R.html 3 KB
divides_nat_ref.html 3 KB
divides_nat_tra.html 11 KB
dneg.html 1 KB
double_SNo_max_1.html 72 KB
double_SNo_min_1.html 26 KB
double_eps_1.html 10 KB
eps_0_1.html 7 KB
eps_1_half_eq1.html 892 bytes
eps_1_half_eq2.html 3 KB
eps_SNoCut.html 89 KB
eps_SNoCutP.html 9 KB
eps_SNo_eq.html 24 KB
eps_bd_1.html 8 KB
eps_diadic_rational_p.html 3 KB
eps_ordinal_In_eq_0.html 6 KB
eps_ordsucc_half_add.html 83 KB
eq_1_Sing0.html 774 bytes
eq_i_tra.html 555 bytes
eq_or_nand.html 5 KB
equip_0_Empty.html 2 KB
equip_Sing_1.html 6 KB
equip_adjoin_ordsucc.html 30 KB
equip_atleastp.html 1 KB
equip_finite_Power.html 157 KB
equip_ordsucc_remove1.html 63 KB
equip_real_Power_omega.html 894 KB
equip_ref.html 1 KB
equip_sym.html 2 KB
equip_tra.html 2 KB
euclidean_algorithm.html 11 KB
euclidean_algorithm_prop_1.html 11 KB
exactly1of2_E.html 2 KB
exactly1of2_I1.html 1 KB
exactly1of2_I2.html 1 KB
exactly1of2_or.html 2 KB
exandE_i.html 1 KB
exandE_ii.html 1 KB
exandE_iii.html 1 KB
exandE_iiii.html 1 KB
exp_SNo_1_bd.html 8 KB
exp_SNo_2_bd.html 16 KB
exp_SNo_nat_0.html 722 bytes
exp_SNo_nat_1.html 2 KB
exp_SNo_nat_S.html 1 KB
exp_SNo_nat_mul_add.html 20 KB
exp_SNo_nat_mul_add__2.html 1 KB
exp_SNo_nat_pos.html 5 KB
exp_nat_0.html 1 KB
exp_nat_1.html 1 KB
exp_nat_S.html 2 KB
exp_nat_p.html 3 KB
famunionE.html 4 KB
famunionE_impred.html 1 KB
famunionI.html 1 KB
famunion_Empty.html 2 KB
famunion_Subq.html 2 KB
famunion_ext.html 2 KB
famunion_nat_finite.html 14 KB
finite_Empty.html 1 KB
finite_ind.html 30 KB
finite_max_exists.html 55 KB
finite_min_exists.html 19 KB
form100_11_infinite_primes.html 44 KB
form100_1_lem1.html 67 KB
form100_1_lem2.html 4 KB
form100_22_real_uncountable.html 3 KB
form100_22_real_uncountable_atleastp.html 4 KB
form100_22_real_uncountable_equip.html 1 KB
form100_22_v1.html 2 KB
form100_22_v2.html 341 bytes
form100_22_v3.html 8 KB
form100_3.html 124 KB
form100_63_injCantor.html 10 KB
form100_63_surjCantor.html 7 KB
gcd_0.html 8 KB
gcd_id.html 29 KB
gcd_minus.html 7 KB
gcd_reln_uniq.html 8 KB
gcd_sym.html 4 KB
iffEL.html 568 bytes
iffER.html 568 bytes
iffI.html 566 bytes
iff_refl.html 902 bytes
iff_sym.html 1 KB
iff_trans.html 2 KB
image_In_Power.html 3 KB
image_monotone.html 2 KB
infiniteRamsey.html 319 KB
infiniteRamsey_lem.html 46 KB
infinite_Finite_Subq_ex.html 43 KB
infinite_bigger.html 8 KB
infinite_remove1.html 7 KB
injI.html 1 KB
inj_comp.html 5 KB
inj_linv.html 3 KB
int_3_cases.html 9 KB
int_SNo.html 1 KB
int_SNo_cases.html 3 KB
int_add_SNo.html 12 KB
int_add_SNo_lem.html 24 KB
int_diadic_rational_p.html 3 KB
int_lin_comb_E.html 3 KB
int_lin_comb_E1.html 1 KB
int_lin_comb_E2.html 1 KB
int_lin_comb_E3.html 1 KB
int_lin_comb_E4.html 1 KB
int_lin_comb_I.html 2 KB
int_lin_comb_sym.html 6 KB
int_minus_SNo.html 3 KB
int_minus_SNo_omega.html 1 KB
int_mul_SNo.html 25 KB
lamE.html 215 bytes
lamI.html 221 bytes
lamI2.html 1 KB
lam_Pi.html 11 KB
least_ordinal_ex.html 5 KB
least_pos_int_lin_comb_divides_int.html 61 KB
least_pos_int_lin_comb_ex.html 74 KB
least_pos_int_lin_comb_gcd.html 20 KB
minus_SNoCut_eq.html 1 KB
minus_SNoCut_eq_lem.html 46 KB
minus_SNo_0.html 2 KB
minus_SNo_Le_contra.html 4 KB
minus_SNo_Lev.html 3 KB
minus_SNo_Lev_lem1.html 75 KB
minus_SNo_Lev_lem2.html 3 KB
minus_SNo_Lt_contra.html 25 KB
minus_SNo_Lt_contra1.html 2 KB
minus_SNo_Lt_contra2.html 2 KB
minus_SNo_SNo.html 5 KB
minus_SNo_SNoCutP.html 1 KB
minus_SNo_SNoCutP_gen.html 14 KB
minus_SNo_SNoS.html 4 KB
minus_SNo_SNoS_omega.html 5 KB
minus_SNo_diadic_rational_p.html 8 KB
minus_SNo_eq.html 12 KB
minus_SNo_invol.html 32 KB
minus_SNo_max_min.html 7 KB
minus_SNo_max_min__2.html 6 KB
minus_SNo_min_max.html 7 KB
minus_SNo_prereal_1.html 8 KB
minus_SNo_prereal_2.html 12 KB
minus_SNo_prop1.html 74 KB
minus_add_SNo_distr.html 13 KB
minus_add_SNo_distr_3.html 2 KB
mordinal_SNoLev_min_2.html 5 KB
mul_SNoCutP_lem.html 594 KB
mul_SNoCut_abs.html 1 KB
mul_SNo_In_omega.html 1 KB
mul_SNo_Le.html 7 KB
mul_SNo_Le1_nonneg_Le.html 1 KB
mul_SNo_Lt.html 234 KB
mul_SNo_Lt1_pos_Lt.html 1 KB
mul_SNo_SNoCut_SNoL_interpolate.html 98 KB
mul_SNo_SNoCut_SNoL_interpolate_impred.html 5 KB
mul_SNo_SNoCut_SNoR_interpolate.html 98 KB
mul_SNo_SNoCut_SNoR_interpolate_impred.html 5 KB
mul_SNo_SNoL_interpolate.html 77 KB
mul_SNo_SNoL_interpolate_impred.html 4 KB
mul_SNo_SNoR_interpolate.html 78 KB
mul_SNo_SNoR_interpolate_impred.html 4 KB
mul_SNo_SNoS_omega.html 1 KB
mul_SNo_Subq_lem.html 3 KB
mul_SNo_assoc.html 106 KB
mul_SNo_assoc_lem1.html 291 KB
mul_SNo_assoc_lem2.html 301 KB
mul_SNo_com.html 66 KB
mul_SNo_com_3_0_1.html 1 KB
mul_SNo_com_3b_1_2.html 1 KB
mul_SNo_com_4_inner_mid.html 4 KB
mul_SNo_diadic_rational_p.html 15 KB
mul_SNo_distrL.html 3 KB
mul_SNo_distrR.html 930 KB
mul_SNo_eps_eps_add_SNo.html 26 KB
mul_SNo_eps_power_2.html 14 KB
mul_SNo_eps_power_2__2.html 2 KB
mul_SNo_eq.html 81 KB
mul_SNo_eq_2.html 72 KB
mul_SNo_eq_3.html 114 KB
mul_SNo_minus_distrL.html 178 KB
mul_SNo_minus_distrR.html 1 KB
mul_SNo_minus_minus.html 3 KB
mul_SNo_neg_neg.html 6 KB
mul_SNo_neg_pos.html 5 KB
mul_SNo_nonneg_nonneg.html 4 KB
mul_SNo_nonpos_neg.html 4 KB
mul_SNo_nonpos_nonneg.html 2 KB
mul_SNo_nonpos_pos.html 4 KB
mul_SNo_nonzero_cancel.html 12 KB
mul_SNo_nonzero_cancel_L.html 5 KB
mul_SNo_oneL.html 1 KB
mul_SNo_oneR.html 60 KB
mul_SNo_pos_neg.html 5 KB
mul_SNo_pos_pos.html 6 KB
mul_SNo_prop_1.html 494 KB
mul_SNo_rotate_3_1.html 3 KB
mul_SNo_zeroL.html 1 KB
mul_SNo_zeroR.html 11 KB
mul_add_nat_distrL.html 15 KB
mul_div_SNo_L.html 2 KB
mul_div_SNo_R.html 10 KB
mul_div_SNo_both.html 4 KB
mul_div_SNo_invL.html 3 KB
mul_div_SNo_invR.html 1 KB
mul_div_SNo_nonzero_eq.html 2 KB
mul_minus_SNo_distrR.html 2 KB
mul_nat_0L.html 3 KB
mul_nat_0R.html 650 bytes
mul_nat_0_inv.html 9 KB
mul_nat_0_or_Subq.html 4 KB
mul_nat_0m_1n_In.html 17 KB
mul_nat_1R.html 1 KB
mul_nat_SL.html 13 KB
mul_nat_SR.html 870 bytes
mul_nat_Subq_L.html 1 KB
mul_nat_Subq_R.html 9 KB
mul_nat_asso.html 9 KB
mul_nat_com.html 6 KB
mul_nat_mul_SNo.html 16 KB
mul_nat_p.html 4 KB
nat_0.html 233 bytes
nat_0_in_ordsucc.html 2 KB
nat_1.html 438 bytes
nat_1In_not_divides_ordsucc.html 20 KB
nat_2.html 438 bytes
nat_Subq_add_ex.html 12 KB
nat_complete_ind.html 7 KB
nat_exp_SNo_nat.html 5 KB
nat_finite.html 1 KB
nat_ind.html 7 KB
nat_inv.html 1 KB
nat_inv_impred.html 773 bytes
nat_le1_cases.html 4 KB
nat_le2_cases.html 7 KB
nat_ordsucc.html 553 bytes
nat_ordsucc_in_ordsucc.html 8 KB
nat_ordsucc_trans.html 3 KB
nat_p_SNo.html 994 bytes
nat_p_UnivOf_Empty.html 2 KB
nat_p_omega.html 2 KB
nat_p_ordinal.html 2 KB
nat_p_trans.html 4 KB
nat_pair_0.html 98 KB
nat_pair_1.html 17 KB
nat_pair_In_omega.html 3 KB
nat_primrec_0.html 4 KB
nat_primrec_S.html 7 KB
nat_primrec_r.html 14 KB
nat_trans.html 6 KB
neg_abs_SNo.html 2 KB
neg_mul_SNo_Lt.html 6 KB
neq_0_1.html 339 bytes
neq_0_2.html 339 bytes
neq_0_ordsucc.html 2 KB
neq_1_0.html 339 bytes
neq_2_0.html 339 bytes
neq_i_sym.html 549 bytes
neq_ordsucc_0.html 801 bytes
nonneg_abs_SNo.html 870 bytes
nonneg_diadic_rational_p_SNoS_omega.html 10 KB
nonneg_int_nat_p.html 8 KB
nonneg_mul_SNo_Le.html 6 KB
nonneg_mul_SNo_Le2.html 5 KB
nonneg_mul_SNo_Le__2.html 1 KB
nonneg_real_nat_interval.html 36 KB
nonpos_mul_SNo_Le.html 7 KB
nonpos_nonneg_0.html 10 KB
not_TransSet_Sing1.html 2 KB
not_all_ex_demorgan_i.html 2 KB
not_eq_2m_2n1.html 18 KB
not_ex_all_demorgan_i.html 885 bytes
not_nonneg_abs_SNo.html 870 bytes
not_or_and_demorgan.html 2 KB
not_ordinal_Sing1.html 644 bytes
omega_SNo.html 773 bytes
omega_SNoS_omega.html 3 KB
omega_TransSet.html 2 KB
omega_diadic_rational_p.html 803 bytes
omega_nat_p.html 730 bytes
omega_nonneg.html 1 KB
omega_ordinal.html 2 KB
omega_ordsucc.html 981 bytes
or3E.html 644 bytes
or3I1.html 804 bytes
or3I2.html 804 bytes
or3I3.html 468 bytes
orIL.html 298 bytes
orIR.html 298 bytes
ordinal_0_In_ordsucc.html 2 KB
ordinal_1.html 413 bytes
ordinal_2.html 413 bytes
ordinal_Empty.html 2 KB
ordinal_Hered.html 4 KB
ordinal_In_Or_Subq.html 4 KB
ordinal_In_SNoLt.html 4 KB
ordinal_SNo.html 7 KB
ordinal_SNoL.html 10 KB
ordinal_SNoLev.html 2 KB
ordinal_SNoLev_max.html 13 KB
ordinal_SNoLev_max_2.html 23 KB
ordinal_SNoLt_In.html 4 KB
ordinal_SNoR.html 5 KB
ordinal_SNo__2.html 1 KB
ordinal_Subq_SNoLe.html 6 KB
ordinal_TransSet.html 834 bytes
ordinal_binintersect.html 3 KB
ordinal_binunion.html 3 KB
ordinal_famunion.html 10 KB
ordinal_ind.html 3 KB
ordinal_lim_or_succ.html 4 KB
ordinal_linear.html 2 KB
ordinal_notin_tagged_Repl.html 2 KB
ordinal_ordsucc.html 5 KB
ordinal_ordsucc_In.html 4 KB
ordinal_ordsucc_In_Subq.html 983 bytes
ordinal_ordsucc_In_eq.html 6 KB
ordinal_ordsucc_SNo_eq.html 1 KB
ordinal_ordsucc_pos.html 1 KB
ordinal_trichotomy_or.html 19 KB
ordinal_trichotomy_or_impred.html 1 KB
ordsuccE.html 2 KB
ordsuccI1.html 855 bytes
ordsuccI2.html 758 bytes
ordsucc_inj.html 5 KB
ordsucc_omega_ordinal.html 450 bytes
pairE.html 705 bytes
pairE0.html 7 KB
pairE1.html 8 KB
pairI0.html 461 bytes
pairI1.html 461 bytes
pair_Sigma.html 4 KB
pair_Sigma_E1.html 3 KB
pair_ap_0.html 1 KB
pair_ap_1.html 1 KB
pair_p_I.html 1 KB
pair_tuple_fun.html 1 KB
pos_abs_SNo.html 995 bytes
pos_low_eq_one.html 15 KB
pos_mul_SNo_Lt.html 6 KB
pos_mul_SNo_Lt2.html 5 KB
pos_mul_SNo_Lt__2.html 1 KB
pos_real_left_approx_double.html 143 KB
pred_ext.html 1 KB
prime_factorization_ex_uniq.html 164 KB
prime_nat_2.html 5 KB
prime_nat_2_lem.html 8 KB
prime_nat_divisor_ex.html 14 KB
prime_nat_or_composite_nat.html 26 KB
prime_not_divides_int_1.html 6 KB
proj0E.html 6 KB
proj0I.html 4 KB
proj0_Sigma.html 2 KB
proj0_ap_0.html 4 KB
proj0_pair_eq.html 5 KB
proj1E.html 6 KB
proj1I.html 4 KB
proj1_Sigma.html 2 KB
proj1_ap_1.html 4 KB
proj1_pair_eq.html 5 KB
prop_ext_2.html 985 bytes
quotient_remainder_int.html 58 KB
quotient_remainder_nat.html 24 KB
rational_minus_SNo.html 21 KB
real_0.html 881 bytes
real_1.html 881 bytes
real_E.html 13 KB
real_I.html 5 KB
real_SNo.html 791 bytes
real_SNoCut.html 137 KB
real_SNoCut_SNoS_omega.html 113 KB
real_SNoS_omega_prop.html 791 bytes
real_add_SNo.html 260 KB
real_div_SNo.html 1 KB
real_minus_SNo.html 9 KB
real_mul_SNo.html 23 KB
real_mul_SNo_pos.html 800 KB
real_recip_SNo.html 8 KB
real_recip_SNo_lem1.html 389 KB
real_recip_SNo_pos.html 1 KB
recip_SNo_0.html 5 KB
recip_SNo_invL.html 1 KB
recip_SNo_invR.html 9 KB
recip_SNo_negcase.html 5 KB
recip_SNo_of_pos_is_pos.html 984 bytes
recip_SNo_pos_2.html 847 bytes
recip_SNo_pos_eps.html 8 KB
recip_SNo_pos_eq.html 8 KB
recip_SNo_pos_invR.html 869 bytes
recip_SNo_pos_invol.html 8 KB
recip_SNo_pos_is_pos.html 8 KB
recip_SNo_pos_pos.html 6 KB
recip_SNo_pos_pow_2.html 1 KB
recip_SNo_pos_prop1.html 364 KB
recip_SNo_poscase.html 1 KB
recip_SNo_pow_2.html 2 KB
restr_SNo.html 18 KB
restr_SNoEq.html 4 KB
restr_SNoLev.html 3 KB
restr_SNo__2.html 3 KB
setminusE.html 689 bytes
setminusE1.html 691 bytes
setminusE2.html 691 bytes
setminusI.html 751 bytes
setminus_In_Power.html 515 bytes
setminus_Subq.html 221 bytes
setminus_antimonotone.html 2 KB
setsum_Inj_inv.html 4 KB
sqrt_2_irrational.html 49 KB
sqrt_SNo_nonneg_0.html 28 KB
sqrt_SNo_nonneg_0inL0.html 9 KB
sqrt_SNo_nonneg_1.html 44 KB
sqrt_SNo_nonneg_Lnonempty.html 5 KB
sqrt_SNo_nonneg_Rnonempty.html 28 KB
sqrt_SNo_nonneg_SNoS_omega.html 176 KB
sqrt_SNo_nonneg_eq.html 8 KB
sqrt_SNo_nonneg_nonneg.html 1 KB
sqrt_SNo_nonneg_prop1.html 36 KB
sqrt_SNo_nonneg_prop1a.html 377 KB
sqrt_SNo_nonneg_prop1b.html 24 KB
sqrt_SNo_nonneg_prop1c.html 11 KB
sqrt_SNo_nonneg_prop1d.html 120 KB
sqrt_SNo_nonneg_prop1e.html 169 KB
sqrt_SNo_nonneg_real.html 175 KB
sqrt_SNo_nonneg_sqr.html 879 bytes
surj_rinv.html 1 KB
tagged_ReplE.html 3 KB
tagged_eqE_Subq.html 4 KB
tagged_eqE_eq.html 1 KB
tagged_not_ordinal.html 2 KB
tagged_notin_ordinal.html 1 KB
tuple_2_0_eq.html 1 KB
tuple_2_1_eq.html 1 KB
tuple_2_Sigma.html 211 bytes
tuple_2_setprod.html 678 bytes
tuple_pair.html 30 KB
xm.html 13 KB