Commit 2023-01-10 06:56 550e2907

View on Github →

feat: port Data.Real.CauSeq (#1124)

depends on: #1398

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/CauSeq.lean

added def CauSeq.LimZero

added def CauSeq.Pos

added theorem CauSeq.abv_pos_of_not_limZero

added theorem CauSeq.add_apply

added theorem CauSeq.add_equiv_add

added theorem CauSeq.add_limZero

added theorem CauSeq.add_pos

added theorem CauSeq.bounded'

added theorem CauSeq.bounded

added theorem CauSeq.cauchy

added theorem CauSeq.cauchy₂

added theorem CauSeq.cauchy₃

added theorem CauSeq.coe_add

added theorem CauSeq.coe_const

added theorem CauSeq.coe_inf

added theorem CauSeq.coe_inv

added theorem CauSeq.coe_mul

added theorem CauSeq.coe_neg

added theorem CauSeq.coe_one

added theorem CauSeq.coe_pow

added theorem CauSeq.coe_smul

added theorem CauSeq.coe_sub

added theorem CauSeq.coe_sup

added theorem CauSeq.coe_zero

added def CauSeq.const

added theorem CauSeq.const_add

added theorem CauSeq.const_apply

added theorem CauSeq.const_equiv

added theorem CauSeq.const_inj

added theorem CauSeq.const_inv

added theorem CauSeq.const_le

added theorem CauSeq.const_limZero

added theorem CauSeq.const_lt

added theorem CauSeq.const_mul

added theorem CauSeq.const_neg

added theorem CauSeq.const_one

added theorem CauSeq.const_pos

added theorem CauSeq.const_pow

added theorem CauSeq.const_smul

added theorem CauSeq.const_sub

added theorem CauSeq.const_zero

added theorem CauSeq.equiv_def₃

added theorem CauSeq.exists_gt

added theorem CauSeq.exists_lt

added theorem CauSeq.ext

added theorem CauSeq.inf_equiv_inf

added theorem CauSeq.inf_limZero

added def CauSeq.inv

added theorem CauSeq.inv_apply

added theorem CauSeq.inv_aux

added theorem CauSeq.inv_mul_cancel

added theorem CauSeq.isCauSeq

added theorem CauSeq.le_antisymm

added theorem CauSeq.le_of_eq_of_le

added theorem CauSeq.le_of_exists

added theorem CauSeq.le_of_le_of_eq

added theorem CauSeq.le_total

added theorem CauSeq.limZero_congr

added theorem CauSeq.limZero_sub_rev

added theorem CauSeq.lt_irrefl

added theorem CauSeq.lt_of_eq_of_lt

added theorem CauSeq.lt_of_lt_of_eq

added theorem CauSeq.lt_total

added theorem CauSeq.lt_trans

added theorem CauSeq.mul_apply

added theorem CauSeq.mul_equiv_mul

added theorem CauSeq.mul_equiv_zero'

added theorem CauSeq.mul_equiv_zero

added theorem CauSeq.mul_inv_cancel

added theorem CauSeq.mul_limZero_left

added theorem CauSeq.mul_limZero_right

added theorem CauSeq.mul_not_equiv_zero

added theorem CauSeq.neg_apply

added theorem CauSeq.neg_equiv_neg

added theorem CauSeq.neg_limZero

added theorem CauSeq.not_limZero_of_not_congr_zero

added theorem CauSeq.not_limZero_of_pos

added def CauSeq.ofEq

added theorem CauSeq.of_near

added theorem CauSeq.one_apply

added theorem CauSeq.one_not_equiv_zero

added theorem CauSeq.pos_add_limZero

added theorem CauSeq.pow_apply

added theorem CauSeq.pow_equiv_pow

added theorem CauSeq.rat_inf_continuous_lemma

added theorem CauSeq.rat_sup_continuous_lemma

added theorem CauSeq.smul_apply

added theorem CauSeq.smul_equiv_smul

added theorem CauSeq.sub_apply

added theorem CauSeq.sub_equiv_sub

added theorem CauSeq.sub_limZero

added theorem CauSeq.sup_equiv_sup

added theorem CauSeq.sup_limZero

added theorem CauSeq.trichotomy

added theorem CauSeq.zero_apply

added theorem CauSeq.zero_limZero

added def CauSeq

added theorem IsCauSeq.add

added theorem IsCauSeq.cauchy₂

added theorem IsCauSeq.cauchy₃

added def IsCauSeq

added theorem exists_forall_ge_and

added theorem rat_add_continuous_lemma

added theorem rat_inv_continuous_lemma

added theorem rat_mul_continuous_lemma