# mathlib3documentation

topology.algebra.order.floor

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) (set.Ici n)) (nhds n)
theorem tendsto_ceil_left' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Iic n)) (nhds n)
theorem tendsto_floor_right {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Ici n)) (set.Ici n))
theorem tendsto_ceil_left {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Iic n)) (set.Iic n))
theorem tendsto_floor_left {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Iio n)) (nhds_within (n - 1) (set.Iic (n - 1)))
theorem tendsto_ceil_right {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Ioi n)) (nhds_within (n + 1) (set.Ici (n + 1)))
theorem tendsto_floor_left' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Iio n)) (nhds (n - 1))
theorem tendsto_ceil_right' {α : Type u_1} [floor_ring α] (n : ) :
filter.tendsto (λ (x : α), x) (set.Ioi n)) (nhds (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 : ) :
(nhds 1)
theorem tendsto_fract_left {α : Type u_1} [floor_ring α] (n : ) :
(set.Iio 1))
theorem tendsto_fract_right' {α : Type u_1} [floor_ring α] (n : ) :
(nhds 0)
theorem tendsto_fract_right {α : Type u_1} [floor_ring α] (n : ) :
(set.Ici 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.