Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-10 07:07 e729ab4a

View on Github →

feat(analysis/specific_limits): limit of nat_floor (a * x) / x (#8549)

Estimated changes

Modified src/algebra/floor.lean

added theorem floor_lt_ceil_of_lt

added theorem nat_floor_lt_nat_ceil_of_lt_of_pos

Modified src/analysis/specific_limits.lean

added theorem tendsto_nat_ceil_mul_div_at_top

added theorem tendsto_nat_floor_mul_div_at_top