# mathlibdocumentation

topology.algebra.floor_ring

# 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_at_top, tendsto_floor_at_bot, tendsto_ceil_at_top, tendsto_ceil_at_bot: int.floor and int.ceil tend to +-∞ in +-∞.
• continuous_on_floor: int.floor is continuous on Ico n (n + 1), because constant.
• continuous_on_ceil: int.ceil is continuous on Ioc n (n + 1), because constant.
• continuous_on_fract: int.fract is continuous on Ico n (n + 1).
• continuous_on.comp_fract: Precomposing a continuous function satisfying f 0 = f 1 with int.fract yields another continuous function.
theorem tendsto_floor_at_top {α : Type u_1} [floor_ring α] :
theorem tendsto_floor_at_bot {α : Type u_1} [floor_ring α] :
theorem tendsto_ceil_at_top {α : Type u_1} [floor_ring α] :
theorem tendsto_ceil_at_bot {α : Type u_1} [floor_ring α] :
theorem continuous_on_floor {α : Type u_1} [floor_ring α] (n : ) :
continuous_on (λ (x : α), x) (set.Ico n (n + 1))
theorem continuous_on_ceil {α : Type u_1} [floor_ring α] (n : ) :
continuous_on (λ (x : α), x) (set.Ioc (n - 1) n)
theorem tendsto_floor_right' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝 n)
theorem tendsto_ceil_left' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝 n)
theorem tendsto_floor_right {α : Type u_1} [floor_ring α] (n : ) :
theorem tendsto_ceil_left {α : Type u_1} [floor_ring α] (n : ) :
theorem tendsto_floor_left {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝[set.Iic (n - 1)] (n - 1))
theorem tendsto_ceil_right {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝[set.Ici (n + 1)] (n + 1))
theorem tendsto_floor_left' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝 (n - 1))
theorem tendsto_ceil_right' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (𝓝[] n) (𝓝 (n + 1))
theorem continuous_on_fract {α : Type u_1} [floor_ring α] (n : ) :
(set.Ico n (n + 1))
theorem tendsto_fract_left' {α : Type u_1} [floor_ring α] (n : ) :
(𝓝 1)
theorem tendsto_fract_left {α : Type u_1} [floor_ring α] (n : ) :
(𝓝[] 1)
theorem tendsto_fract_right' {α : Type u_1} [floor_ring α] (n : ) :
(𝓝 0)
theorem tendsto_fract_right {α : Type u_1} [floor_ring α] (n : ) :
(𝓝[] 0)
theorem continuous_on.comp_fract' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [floor_ring α] {f : β → α → γ} (h : (set.univ ×ˢ 1)) (hf : ∀ (s : β), f s 0 = f s 1) :
continuous (λ (st : β × α), f st.fst (int.fract st.snd))

Do not use this, use continuous_on.comp_fract instead.

theorem continuous_on.comp_fract {α : Type u_1} {β : Type u_2} {γ : Type u_3} [floor_ring α] {s : β → α} {f : β → α → γ} (h : (set.univ ×ˢ 1)) (hs : continuous s) (hf : ∀ (s : β), f s 0 = f s 1) :
continuous (λ (x : β), f x (int.fract (s x)))
theorem continuous_on.comp_fract'' {α : Type u_1} {β : Type u_2} [floor_ring α] {f : α → β} (h : (set.Icc 0 1)) (hf : f 0 = f 1) :

A special case of continuous_on.comp_fract.