Hyperreal 📖 | CompOp | 121 mathmath: Hyperreal.InfiniteNeg.neg, Hyperreal.infinitePos_add_not_infiniteNeg, Hyperreal.infinite_neg, Hyperreal.epsilon_lt_of_pos, Hyperreal.not_infinite_zero, Hyperreal.neg_lt_of_tendsto_zero_of_pos, Hyperreal.not_infiniteNeg_add_infinitePos, Hyperreal.epsilon_mul_omega, Hyperreal.not_infinitePos_add_infiniteNeg, Hyperreal.coe_ofNat, Hyperreal.InfinitePos.neg, Hyperreal.infinitesimal_def, Hyperreal.coe_lt_omega, Hyperreal.Infinitesimal.add, Hyperreal.InfiniteNeg.lt_zero, Hyperreal.Infinite.mul, Hyperreal.infinitePos_add_not_infinite, Hyperreal.infinitesimal_inv_of_infinite, Hyperreal.infinite_abs_iff, Hyperreal.infinite_mul_of_not_infinitesimal_infinite, Hyperreal.not_infinite_iff_exist_lt_gt, Hyperreal.archimdeanClassMk_coe, Hyperreal.tendsto_iff_forall, Hyperreal.inv_omega, Hyperreal.infinite_iff_infinitesimal_inv, Hyperreal.infinitePos_neg, Hyperreal.isSt_iff_abs_sub_lt_delta, Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot, Hyperreal.isSt_sSup, Hyperreal.coe_eq_one, Hyperreal.st_mul, Hyperreal.stdPart_coe, Hyperreal.infinitePos_iff_infinite_and_pos, Hyperreal.epsilon_lt_pos, Hyperreal.coe_nonneg, Hyperreal.infiniteNeg_mul_infiniteNeg, Hyperreal.infinitePos_iff_infinitesimal_inv_pos, Hyperreal.coe_pos, Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop, Hyperreal.IsSt.add, Hyperreal.infiniteNeg_iff_infinite_and_neg, Hyperreal.lt_of_tendsto_atTop, Hyperreal.archimedeanClassMk_pos_of_tendsto, Hyperreal.infinitesimal_sub_st, Hyperreal.infinitePos_abs_iff_infinite_abs, Hyperreal.inv_epsilon, Hyperreal.archimedeanClassMk_nonneg_of_tendsto, Hyperreal.epsilon_lt_of_neg, Hyperreal.IsSt.mul, Hyperreal.IsSt.inv, Hyperreal.infinitePos_mul_infiniteNeg, Hyperreal.coe_inv, Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv, Hyperreal.infiniteNeg_def, Hyperreal.infiniteNeg_mul_infinitePos, Hyperreal.IsSt.sub, Hyperreal.Infinitesimal.mul, Hyperreal.instIsStrictOrderedRing, Hyperreal.coe_eq_zero, Hyperreal.coe_zero, Hyperreal.coe_min, Hyperreal.lt_neg_of_pos_of_infinitesimal, Hyperreal.infinitesimal_iff_infinite_inv, Hyperreal.ofSeq_surjective, Hyperreal.not_infinite_neg, Hyperreal.lt_of_pos_of_infinitesimal, Hyperreal.infiniteNeg_add_infiniteNeg, Hyperreal.not_infinite_add, Hyperreal.coe_one, Hyperreal.lt_of_tendsto_atBot, Hyperreal.infinite_mul_of_infinite_not_infinitesimal, Hyperreal.infinite_iff_abs_lt_abs, Hyperreal.ofSeq_le_ofSeq, Hyperreal.omega_pos, Hyperreal.coe_add, Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg, Hyperreal.archimedeanClassMk_omega_neg, Hyperreal.archimedeanClassMk_coe_nonneg, Hyperreal.tendsto_atBot_iff, Hyperreal.lt_of_tendsto_zero_of_pos, Hyperreal.coe_max, Hyperreal.not_infinite_mul, Hyperreal.stdPart_of_tendsto, Hyperreal.infinitesimal_zero, Hyperreal.coe_div, Hyperreal.lt_of_st_lt, Hyperreal.infiniteNeg_neg, Hyperreal.coe_abs, Hyperreal.st_inv, Hyperreal.IsSt.lt, Hyperreal.abs_omega, Hyperreal.InfinitePos.pos, Hyperreal.infinitePos_def, Hyperreal.infinitesimal_neg, Hyperreal.coe_neg, Hyperreal.stdPart_omega, Hyperreal.abs_lt_real_iff_infinitesimal, Hyperreal.infinitesimal_pos_iff_infinitePos_inv, Hyperreal.coe_mul, Hyperreal.coe_le_coe, Hyperreal.infiniteNeg_add_not_infinitePos, Hyperreal.coe_lt_coe, Hyperreal.infinitePos_add_infinitePos, Hyperreal.st_eq_sSup, Hyperreal.infinitePos_abs_iff_infinite, Hyperreal.IsSt.neg, Hyperreal.infinitePos_mul_infinitePos, Hyperreal.stdPart_epsilon, Hyperreal.ofSeq_lt_ofSeq, Hyperreal.st_neg, Hyperreal.gt_of_neg_of_infinitesimal, Hyperreal.st_add, Hyperreal.coe_sub, Hyperreal.infiniteNeg_add_not_infinite, Hyperreal.gt_of_tendsto_zero_of_neg, Hyperreal.epsilon_pos, Hyperreal.archimedeanClassMk_epsilon_pos, Hyperreal.IsSt.infinitesimal_sub, Hyperreal.tendsto_atTop_iff, Hyperreal.Infinitesimal.neg, Hyperreal.coeRingHom_toFun
|