mathlib3 documentation

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 #

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} {β : Type u_2} {γ : Type u_3} [linear_ordered_ring α] [floor_ring α] [topological_space α] [order_topology α] [topological_space β] [topological_space γ] {f : β α γ} (h : continuous_on (function.uncurry f) (set.univ ×ˢ set.Icc 0 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} [linear_ordered_ring α] [floor_ring α] [topological_space α] [order_topology α] [topological_space β] [topological_space γ] {s : β α} {f : β α γ} (h : continuous_on (function.uncurry f) (set.univ ×ˢ set.Icc 0 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} [linear_ordered_ring α] [floor_ring α] [topological_space α] [order_topology α] [topological_space β] {f : α β} (h : continuous_on f (set.Icc 0 1)) (hf : f 0 = f 1) :

A special case of continuous_on.comp_fract.