Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-07 13:36 c259305a

View on Github →

feat(topology/algebra/floor_ring): add basic topological facts about floor, ceil and fract (#4042) From the sphere eversion project

Estimated changes

added theorem ceil_eq_iff
added theorem ceil_eq_on_Ioc'
added theorem ceil_eq_on_Ioc
added theorem floor_eq_on_Ico'
added theorem floor_eq_on_Ico
added theorem continuous_on_ceil
added theorem continuous_on_floor
added theorem continuous_on_fract
added theorem tendsto_ceil_at_bot
added theorem tendsto_ceil_at_top
added theorem tendsto_ceil_left'
added theorem tendsto_ceil_left
added theorem tendsto_ceil_right'
added theorem tendsto_ceil_right
added theorem tendsto_floor_at_bot
added theorem tendsto_floor_at_top
added theorem tendsto_floor_left'
added theorem tendsto_floor_left
added theorem tendsto_floor_right'
added theorem tendsto_floor_right
added theorem tendsto_fract_left'
added theorem tendsto_fract_left
added theorem tendsto_fract_right'
added theorem tendsto_fract_right