audit-session038-axioms.txt
23 declarations audited · 3 standard axioms only · updated 08-25-2026
Raw #print axioms transcript
'NguyenRH1.sigmaP_eq_neg_iteratedDeriv_gFun_div' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sigmaP_one_eq_neg_gFun_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_seriesFun_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTerm_deriv_summableLocallyUniformlyOn' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_seriesTerm' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iteratedDeriv_zpow_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_eventuallyEq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.xiL_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_eq_momentB' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.gFun_one_eq_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.two_mul_sigmaP_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.vTerm_tsum_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sigmaP_eq_unpaired' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_mult_div_norm_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_mult_inv_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_mult_div_norm_sq_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_mult_one_div_mul_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_mult_vTerm' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_norm_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_one' depends on axioms: [propext, Classical.choice, Quot.sound]