mathlib documentation

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 #

theorem continuous_on_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] [topological_space α] (n : ) :
continuous_on (λ (x : α), x) (set.Ico n (n + 1))
theorem continuous_on_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] [topological_space α] (n : ) :
continuous_on (λ (x : α), x) (set.Ioc (n - 1) n)
theorem continuous_on.comp_fract' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] [topological_space α] {β : Type u_2} {γ : Type u_3} [order_topology α] [topological_add_group α] [topological_space β] [topological_space γ] {f : β → α → γ} (h : continuous_on (function.uncurry f) (set.univ.prod (set.Icc 0 1))) (hf : ∀ (s : β), f s 0 = f s 1) :
continuous (λ (st : β × α), f st.fst (int.fract st.snd))
theorem continuous_on.comp_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] [topological_space α] {β : Type u_2} [order_topology α] [topological_add_group α] [topological_space β] {f : α → β} (h : continuous_on f (set.Icc 0 1)) (hf : f 0 = f 1) :