# Documentation

Mathlib.Topology.Algebra.Order.Floor

# Topological facts about Int.floor, Int.ceil and Int.fract#

This file proves statements about limits and continuity of functions involving floor, ceil and fract.

## Main declarations #

• tendsto_floor_atTop, tendsto_floor_atBot, tendsto_ceil_atTop, tendsto_ceil_atBot: Int.floor and Int.ceil tend to +-∞ in +-∞.
• continuousOn_floor: Int.floor is continuous on Ico n (n + 1), because constant.
• continuousOn_ceil: Int.ceil is continuous on Ioc n (n + 1), because constant.
• continuousOn_fract: Int.fract is continuous on Ico n (n + 1).
• ContinuousOn.comp_fract: Precomposing a continuous function satisfying f 0 = f 1 with Int.fract yields another continuous function.
theorem tendsto_floor_atTop {α : Type u_1} [] :
Filter.Tendsto Int.floor Filter.atTop Filter.atTop
theorem tendsto_floor_atBot {α : Type u_1} [] :
Filter.Tendsto Int.floor Filter.atBot Filter.atBot
theorem tendsto_ceil_atTop {α : Type u_1} [] :
Filter.Tendsto Int.ceil Filter.atTop Filter.atTop
theorem tendsto_ceil_atBot {α : Type u_1} [] :
Filter.Tendsto Int.ceil Filter.atBot Filter.atBot
theorem continuousOn_floor {α : Type u_1} [] [] (n : ) :
ContinuousOn (fun x => x) (Set.Ico (n) (n + 1))
theorem continuousOn_ceil {α : Type u_1} [] [] (n : ) :
ContinuousOn (fun x => x) (Set.Ioc (n - 1) n)
theorem tendsto_floor_right_pure_floor {α : Type u_1} [] [] (x : α) :
Filter.Tendsto Int.floor (nhdsWithin x ()) ()
theorem tendsto_floor_right_pure {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.floor (nhdsWithin (n) (Set.Ici n)) (pure n)
theorem tendsto_ceil_left_pure_ceil {α : Type u_1} [] [] (x : α) :
Filter.Tendsto Int.ceil (nhdsWithin x ()) ()
theorem tendsto_ceil_left_pure {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.ceil (nhdsWithin (n) (Set.Iic n)) (pure n)
theorem tendsto_floor_left_pure_ceil_sub_one {α : Type u_1} [] [] (x : α) :
Filter.Tendsto Int.floor (nhdsWithin x ()) (pure (x - 1))
theorem tendsto_floor_left_pure_sub_one {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.floor (nhdsWithin (n) (Set.Iio n)) (pure (n - 1))
theorem tendsto_ceil_right_pure_floor_add_one {α : Type u_1} [] [] (x : α) :
Filter.Tendsto Int.ceil (nhdsWithin x ()) (pure (x + 1))
theorem tendsto_ceil_right_pure_add_one {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.ceil (nhdsWithin (n) (Set.Ioi n)) (pure (n + 1))
theorem tendsto_floor_right {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Ici n)) (nhdsWithin (n) (Set.Ici n))
theorem tendsto_floor_right' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Ici n)) (nhds n)
theorem tendsto_ceil_left {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Iic n)) (nhdsWithin (n) (Set.Iic n))
theorem tendsto_ceil_left' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Iic n)) (nhds n)
theorem tendsto_floor_left {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Iio n)) (nhdsWithin (n - 1) (Set.Iic (n - 1)))
theorem tendsto_ceil_right {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Ioi n)) (nhdsWithin (n + 1) (Set.Ici (n + 1)))
theorem tendsto_floor_left' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Iio n)) (nhds (n - 1))
theorem tendsto_ceil_right' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto (fun x => x) (nhdsWithin (n) (Set.Ioi n)) (nhds (n + 1))
theorem continuousOn_fract {α : Type u_1} [] [] (n : ) :
ContinuousOn Int.fract (Set.Ico (n) (n + 1))
theorem continuousAt_fract {α : Type u_1} [] [] {x : α} (h : x x) :
ContinuousAt Int.fract x
theorem tendsto_fract_left' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.fract (nhdsWithin (n) (Set.Iio n)) (nhds 1)
theorem tendsto_fract_left {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.fract (nhdsWithin (n) (Set.Iio n)) (nhdsWithin 1 ())
theorem tendsto_fract_right' {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.fract (nhdsWithin (n) (Set.Ici n)) (nhds 0)
theorem tendsto_fract_right {α : Type u_1} [] [] (n : ) :
Filter.Tendsto Int.fract (nhdsWithin (n) (Set.Ici n)) (nhdsWithin 0 ())
theorem ContinuousOn.comp_fract' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {f : βαγ} (h : ContinuousOn () (Set.univ ×ˢ Set.Icc 0 1)) (hf : ∀ (s : β), f s 0 = f s 1) :
Continuous fun st => f st.fst (Int.fract st.snd)

Do not use this, use ContinuousOn.comp_fract instead.

theorem ContinuousOn.comp_fract {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] [] {s : βα} {f : βαγ} (h : ContinuousOn () (Set.univ ×ˢ Set.Icc 0 1)) (hs : ) (hf : ∀ (s : β), f s 0 = f s 1) :
Continuous fun x => f x (Int.fract (s x))
theorem ContinuousOn.comp_fract'' {α : Type u_1} {β : Type u_2} [] [] [] [] {f : αβ} (h : ContinuousOn f (Set.Icc 0 1)) (hf : f 0 = f 1) :
Continuous (f Int.fract)

A special case of ContinuousOn.comp_fract.