# mathlibdocumentation

topology.algebra.floor_ring

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} [floor_ring α] {β : Type u_2} {γ : Type u_3} {f : β → α → γ} (h : (set.univ.prod (set.Icc 0 1))) (hf : ∀ (s : β), f s 0 = f s 1) :
continuous (λ (st : β × α), f st.fst (fract st.snd))
theorem continuous_on.comp_fract {α : Type u_1} [floor_ring α] {β : Type u_2} {f : α → β} (h : (set.Icc 0 1)) (hf : f 0 = f 1) :