Commit 2023-04-24 22:52 63206757

View on Github →

feat: port Data.Real.Hyperreal (#3586)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Hyperreal.lean

added theorem Hyperreal.Infinite.mul

added theorem Hyperreal.Infinite.ne_real

added theorem Hyperreal.Infinite.ne_zero

added theorem Hyperreal.Infinite.not_infinitesimal

added theorem Hyperreal.Infinite.st_eq

added def Hyperreal.Infinite

added theorem Hyperreal.InfiniteNeg.lt_zero

added theorem Hyperreal.InfiniteNeg.neg

added theorem Hyperreal.InfiniteNeg.not_infinitePos

added theorem Hyperreal.InfiniteNeg.not_infinitesimal

added def Hyperreal.InfiniteNeg

added theorem Hyperreal.InfinitePos.neg

added theorem Hyperreal.InfinitePos.not_infiniteNeg

added theorem Hyperreal.InfinitePos.not_infinitesimal

added theorem Hyperreal.InfinitePos.pos

added def Hyperreal.InfinitePos

added theorem Hyperreal.Infinitesimal.eq_zero

added def Hyperreal.Infinitesimal

added theorem Hyperreal.IsSt.add

added theorem Hyperreal.IsSt.infinitesimal_sub

added theorem Hyperreal.IsSt.inv

added theorem Hyperreal.IsSt.isSt_st

added theorem Hyperreal.IsSt.le

added theorem Hyperreal.IsSt.map

added theorem Hyperreal.IsSt.map₂

added theorem Hyperreal.IsSt.mul

added theorem Hyperreal.IsSt.neg

added theorem Hyperreal.IsSt.not_infinite

added theorem Hyperreal.IsSt.st_eq

added theorem Hyperreal.IsSt.sub

added theorem Hyperreal.IsSt.unique

added def Hyperreal.IsSt

added theorem Hyperreal.abs_lt_real_iff_infinitesimal

added theorem Hyperreal.coe_abs

added theorem Hyperreal.coe_add

added theorem Hyperreal.coe_div

added theorem Hyperreal.coe_eq_coe

added theorem Hyperreal.coe_eq_one

added theorem Hyperreal.coe_eq_zero

added theorem Hyperreal.coe_inv

added theorem Hyperreal.coe_le_coe

added theorem Hyperreal.coe_lt_coe

added theorem Hyperreal.coe_max

added theorem Hyperreal.coe_min

added theorem Hyperreal.coe_mul

added theorem Hyperreal.coe_ne_coe

added theorem Hyperreal.coe_ne_one

added theorem Hyperreal.coe_ne_zero

added theorem Hyperreal.coe_neg

added theorem Hyperreal.coe_nonneg

added theorem Hyperreal.coe_ofNat

added theorem Hyperreal.coe_one

added theorem Hyperreal.coe_pos

added theorem Hyperreal.coe_sub

added theorem Hyperreal.coe_zero

added theorem Hyperreal.epsilon_lt_pos

added theorem Hyperreal.epsilon_mul_omega

added theorem Hyperreal.epsilon_ne_zero

added theorem Hyperreal.epsilon_pos

added theorem Hyperreal.eq_of_isSt_real

added theorem Hyperreal.exists_st_iff_not_infinite

added theorem Hyperreal.exists_st_of_not_infinite

added theorem Hyperreal.gt_of_neg_of_infinitesimal

added theorem Hyperreal.gt_of_tendsto_zero_of_neg

added theorem Hyperreal.infiniteNeg_add_infiniteNeg

added theorem Hyperreal.infiniteNeg_add_not_infinite

added theorem Hyperreal.infiniteNeg_add_not_infinitePos

added theorem Hyperreal.infiniteNeg_def

added theorem Hyperreal.infiniteNeg_iff_infinite_and_neg

added theorem Hyperreal.infiniteNeg_iff_infinite_of_neg

added theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg

added theorem Hyperreal.infiniteNeg_mul_infiniteNeg

added theorem Hyperreal.infiniteNeg_mul_infinitePos

added theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos

added theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg

added theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos

added theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg

added theorem Hyperreal.infiniteNeg_neg

added theorem Hyperreal.infiniteNeg_of_tendsto_bot

added theorem Hyperreal.infinitePos_abs_iff_infinite

added theorem Hyperreal.infinitePos_abs_iff_infinite_abs

added theorem Hyperreal.infinitePos_add_infinitePos

added theorem Hyperreal.infinitePos_add_not_infinite

added theorem Hyperreal.infinitePos_add_not_infiniteNeg

added theorem Hyperreal.infinitePos_def

added theorem Hyperreal.infinitePos_iff_infinite_and_pos

added theorem Hyperreal.infinitePos_iff_infinite_of_nonneg

added theorem Hyperreal.infinitePos_iff_infinite_of_pos

added theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos

added theorem Hyperreal.infinitePos_mul_infiniteNeg

added theorem Hyperreal.infinitePos_mul_infinitePos

added theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg

added theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos

added theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg

added theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos

added theorem Hyperreal.infinitePos_neg

added theorem Hyperreal.infinitePos_of_tendsto_top

added theorem Hyperreal.infinitePos_omega

added theorem Hyperreal.infinite_abs_iff

added theorem Hyperreal.infinite_iff_abs_lt_abs

added theorem Hyperreal.infinite_iff_infinitesimal_inv

added theorem Hyperreal.infinite_iff_not_exists_st

added theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal

added theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite

added theorem Hyperreal.infinite_neg

added theorem Hyperreal.infinite_of_infinitesimal_inv

added theorem Hyperreal.infinite_omega

added theorem Hyperreal.infinitesimal_def

added theorem Hyperreal.infinitesimal_epsilon

added theorem Hyperreal.infinitesimal_iff_infinite_inv

added theorem Hyperreal.infinitesimal_inv_of_infinite

added theorem Hyperreal.infinitesimal_neg

added theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv

added theorem Hyperreal.infinitesimal_of_tendsto_zero

added theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv

added theorem Hyperreal.infinitesimal_real_iff

added theorem Hyperreal.infinitesimal_sub_st

added theorem Hyperreal.infinitesimal_zero

added theorem Hyperreal.inv_epsilon

added theorem Hyperreal.inv_omega

added theorem Hyperreal.isSt_iff_abs_sub_lt_delta

added theorem Hyperreal.isSt_iff_tendsto

added theorem Hyperreal.isSt_inj_real

added theorem Hyperreal.isSt_ofSeq_iff_tendsto

added theorem Hyperreal.isSt_of_tendsto

added theorem Hyperreal.isSt_real_iff_eq

added theorem Hyperreal.isSt_refl_real

added theorem Hyperreal.isSt_st'

added theorem Hyperreal.isSt_st

added theorem Hyperreal.isSt_st_of_exists_st

added theorem Hyperreal.isSt_supₛ

added theorem Hyperreal.isSt_symm_real

added theorem Hyperreal.isSt_trans_real

added theorem Hyperreal.lt_neg_of_pos_of_infinitesimal

added theorem Hyperreal.lt_of_pos_of_infinitesimal

added theorem Hyperreal.lt_of_st_lt

added theorem Hyperreal.lt_of_tendsto_zero_of_pos

added theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos

added theorem Hyperreal.not_infiniteNeg_add_infinitePos

added theorem Hyperreal.not_infinitePos_add_infiniteNeg

added theorem Hyperreal.not_infinite_add

added theorem Hyperreal.not_infinite_iff_exist_lt_gt

added theorem Hyperreal.not_infinite_mul

added theorem Hyperreal.not_infinite_neg

added theorem Hyperreal.not_infinite_of_exists_st

added theorem Hyperreal.not_infinite_real

added theorem Hyperreal.not_infinite_zero

added theorem Hyperreal.not_real_of_infinitesimal_ne_zero

added def Hyperreal.ofReal

added def Hyperreal.ofSeq

added theorem Hyperreal.ofSeq_lt_ofSeq

added theorem Hyperreal.ofSeq_surjective

added theorem Hyperreal.omega_ne_zero

added theorem Hyperreal.omega_pos

added theorem Hyperreal.st_add

added theorem Hyperreal.st_eq_supₛ

added theorem Hyperreal.st_id_real

added theorem Hyperreal.st_inv

added theorem Hyperreal.st_le_of_le

added theorem Hyperreal.st_mul

added theorem Hyperreal.st_neg

added def Hyperreal

Modified Mathlib/Order/Filter/FilterProduct.lean

Modified Mathlib/Order/Filter/Ultrafilter.lean

added theorem Nat.hyperfilter_le_atTop