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 #

theorem tendsto_floor_atTop {α : Type u_1} [LinearOrderedRing α] [FloorRing α] :
Filter.Tendsto Int.floor Filter.atTop Filter.atTop
theorem tendsto_floor_atBot {α : Type u_1} [LinearOrderedRing α] [FloorRing α] :
Filter.Tendsto Int.floor Filter.atBot Filter.atBot
theorem tendsto_ceil_atTop {α : Type u_1} [LinearOrderedRing α] [FloorRing α] :
Filter.Tendsto Int.ceil Filter.atTop Filter.atTop
theorem tendsto_ceil_atBot {α : Type u_1} [LinearOrderedRing α] [FloorRing α] :
Filter.Tendsto Int.ceil Filter.atBot Filter.atBot
theorem continuousOn_floor {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] (n : ) :
ContinuousOn (fun (x : α) => x) (Set.Ico (n) (n + 1))
theorem continuousOn_ceil {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] (n : ) :
ContinuousOn (fun (x : α) => x) (Set.Ioc (n - 1) n)
theorem tendsto_floor_right {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Ici n)) (nhdsWithin (n) (Set.Ici n))
theorem tendsto_floor_right' {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Ici n)) (nhds n)
theorem tendsto_ceil_left {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Iic n)) (nhdsWithin (n) (Set.Iic n))
theorem tendsto_ceil_left' {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Iic n)) (nhds n)
theorem tendsto_floor_left {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (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} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (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} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Iio n)) (nhds (n - 1))
theorem tendsto_ceil_right' {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] (n : ) :
Filter.Tendsto (fun (x : α) => x) (nhdsWithin (n) (Set.Ioi n)) (nhds (n + 1))
theorem continuousOn_fract {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [TopologicalAddGroup α] (n : ) :
ContinuousOn Int.fract (Set.Ico (n) (n + 1))
theorem continuousAt_fract {α : Type u_1} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderClosedTopology α] [TopologicalAddGroup α] {x : α} (h : x x) :
ContinuousAt Int.fract x
theorem ContinuousOn.comp_fract' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {f : βαγ} (h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)) (hf : ∀ (s : β), f s 0 = f s 1) :
Continuous fun (st : β × α) => f st.1 (Int.fract st.2)

Do not use this, use ContinuousOn.comp_fract instead.

theorem ContinuousOn.comp_fract {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {s : βα} {f : βαγ} (h : ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1)) (hs : Continuous s) (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} [LinearOrderedRing α] [FloorRing α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] {f : αβ} (h : ContinuousOn f (Set.Icc 0 1)) (hf : f 0 = f 1) :
Continuous (f Int.fract)

A special case of ContinuousOn.comp_fract.