Commit 2023-01-24 20:00 bcba60ea

View on Github →

feat: port Order.Filter.Archimedean (#1818)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Archimedean.lean

added theorem Filter.Tendsto.atBot_mul_const'

added theorem Filter.Tendsto.atBot_mul_neg_const'

added theorem Filter.Tendsto.atBot_zsmul_const

added theorem Filter.Tendsto.atBot_zsmul_neg_const

added theorem Filter.Tendsto.atTop_mul_const'

added theorem Filter.Tendsto.atTop_mul_neg_const'

added theorem Filter.Tendsto.atTop_nsmul_const

added theorem Filter.Tendsto.atTop_nsmul_neg_const

added theorem Filter.Tendsto.atTop_zsmul_const

added theorem Filter.Tendsto.atTop_zsmul_neg_const

added theorem Filter.Tendsto.const_mul_atTop'

added theorem Int.comap_cast_atBot

added theorem Int.comap_cast_atTop

added theorem Nat.comap_cast_atTop

added theorem Rat.comap_cast_atBot

added theorem Rat.comap_cast_atTop

added theorem atBot_hasCountableBasis_of_archimedean

added theorem atTop_hasAntitoneBasis_of_archimedean

added theorem atTop_hasCountableBasis_of_archimedean

added theorem tendsto_int_cast_atBot_iff

added theorem tendsto_int_cast_atTop_atTop

added theorem tendsto_int_cast_atTop_iff

added theorem tendsto_nat_cast_atTop_atTop

added theorem tendsto_nat_cast_atTop_iff

added theorem tendsto_rat_cast_atBot_iff

added theorem tendsto_rat_cast_atTop_iff