Commit 2023-02-27 13:07 13f9beb8

View on Github →

feat: port Topology.Algebra.Order.Floor (#2485) I added some lemmas about Filter.Tendsto _ _ (pure _). These are not simp lemmas, so I think it's OK to not backport them.

Estimated changes

added theorem continuousAt_fract
added theorem continuousOn_ceil
added theorem continuousOn_floor
added theorem continuousOn_fract
added theorem tendsto_ceil_atBot
added theorem tendsto_ceil_atTop
added theorem tendsto_ceil_left'
added theorem tendsto_ceil_left
added theorem tendsto_ceil_left_pure
added theorem tendsto_ceil_right'
added theorem tendsto_ceil_right
added theorem tendsto_floor_atBot
added theorem tendsto_floor_atTop
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