<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>

Basic topological facts (limits and continuity) about `floor`,
`ceil` and `fract` in a `floor_ring`.
-/
import topology.algebra.ordered.basic
import algebra.floor

open set function filter
open_locale topological_space

variables {α : Type*} [linear_ordered_ring α] [floor_ring α]

lemma tendsto_floor_at_top : tendsto (floor : α → ℤ) at_top at_top :=
begin
  refine monotone.tendsto_at_top_at_top (λ a b hab, floor_mono hab) (λ b, _),
  use (b : α) + ((1 : ℤ) : α),
  rw [floor_add_int, floor_coe],
  exact (lt_add_one _).le
end

lemma tendsto_floor_at_bot : tendsto (floor : α → ℤ) at_bot at_bot :=
begin
  refine monotone.tendsto_at_bot_at_bot (λ a b hab, floor_mono hab) (λ b, ⟨b, _⟩),
  rw floor_coe
end

lemma tendsto_ceil_at_top : tendsto (ceil : α → ℤ) at_top at_top :=
tendsto_neg_at_bot_at_top.comp (tendsto_floor_at_bot.comp tendsto_neg_at_top_at_bot)

lemma tendsto_ceil_at_bot : tendsto (ceil : α → ℤ) at_bot at_bot :=
tendsto_neg_at_top_at_bot.comp (tendsto_floor_at_top.comp tendsto_neg_at_bot_at_top)

variables [topological_space α]

lemma continuous_on_floor (n : ℤ) : continuous_on (λ x, floor x : α → α) (Ico n (n+1) : set α) :=
(continuous_on_congr $ floor_eq_on_Ico' n).mpr continuous_on_const

lemma continuous_on_ceil (n : ℤ) : continuous_on (λ x, ceil x : α → α) (Ioc (n-1) n : set α) :=
(continuous_on_congr $ ceil_eq_on_Ioc' n).mpr continuous_on_const

lemma tendsto_floor_right' [order_closed_topology α] (n : ℤ) :
  tendsto (λ x, floor x : α → α) (𝓝[Ici n] n) (𝓝 n) :=
begin
  rw ← nhds_within_Ico_eq_nhds_within_Ici (lt_add_one (n : α)),
  simpa only [floor_coe] using
    (continuous_on_floor n _ (left_mem_Ico.mpr $ lt_add_one (_ : α))).tendsto
end

lemma tendsto_ceil_left' [order_closed_topology α] (n : ℤ) :
  tendsto (λ x, ceil x : α → α) (𝓝[Iic n] n) (𝓝 n) :=
begin
  rw ← nhds_within_Ioc_eq_nhds_within_Iic (sub_one_lt (n : α)),<commit_msg>docs(topology/algebra/floor_ring): add module docstring (#8969)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import algebra.floor
import topology.algebra.ordered.basic

/-!
# Topological facts about `floor`, `ceil` and `fract`

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`:
  `floor` and `ceil` tend to +-∞ in +-∞.
* `continuous_on_floor`: `floor` is continuous on `Ico n (n + 1)`, because constant.
* `continuous_on_ceil`: `ceil` is continuous on `Ioc n (n + 1)`, because constant.
* `continuous_on_fract`: `fract` is continuous on `Ico n (n + 1)`.
* `continuous_on.comp_fract`: Precomposing a continuous function satisfying `f 0 = f 1` with `fract`
  yields another continuous function.
-/

open set function filter
open_locale topological_space

variables {α : Type*} [linear_ordered_ring α] [floor_ring α]

lemma tendsto_floor_at_top : tendsto (floor : α → ℤ) at_top at_top :=
begin
  refine monotone.tendsto_at_top_at_top (λ a b hab, floor_mono hab) (λ b, _),
  use (b : α) + ((1 : ℤ) : α),
  rw [floor_add_int, floor_coe],
  exact (lt_add_one _).le
end

lemma tendsto_floor_at_bot : tendsto (floor : α → ℤ) at_bot at_bot :=
monotone.tendsto_at_bot_at_bot (λ a b, floor_mono) (λ b, ⟨b, (floor_coe _).le⟩)

lemma tendsto_ceil_at_top : tendsto (ceil : α → ℤ) at_top at_top :=
tendsto_neg_at_bot_at_top.comp (tendsto_floor_at_bot.comp tendsto_neg_at_top_at_bot)

lemma tendsto_ceil_at_bot : tendsto (ceil : α → ℤ) at_bot at_bot :=
tendsto_neg_at_top_at_bot.comp (tendsto_floor_at_top.comp tendsto_neg_at_bot_at_top)

variables [topological_space α]

lemma continuous_on_floor (n : ℤ) : continuous_on (λ x, floor x : α → α) (Ico n (n+1) : set α) :=
(continuous_on_congr $ floor_eq_on_Ico' n).mpr continuous_on_const

lemma continuous_on_ceil (n : ℤ) : continuous_on (λ x, ceil x : α → α) (Ioc (n-1) n : set α) :=
(continuous_on_congr $ ceil_eq_on_Ioc' n).mpr continuous_on_const

lemma tendsto_floor_right' [order_closed_topology α] (n : ℤ) :
  tendsto (λ x, floor x : α → α) (𝓝[Ici n] n) (𝓝 n) :=
begin
  rw ← nhds_within_Ico_eq_nhds_within_Ici (lt_add_one (n : α)),
  simpa only [floor_coe] using
    (continuous_on_floor n _ (left_mem_Ico.mpr $ lt_add_one (_ : α))).tendsto
end

lemma tendsto_ceil_left' [order_closed_topology α] (n : ℤ) :
  tendsto (λ x, ceil x : α → α) (𝓝[Iic n] n) (𝓝 n) :=
begin
  rw ← nhds_within_Ioc_eq_nhds_within_Iic (sub_one_lt (n : α)),
{'fraction_non_alphanumeric': 0.11701900491138159, 'fraction_numerical': 0.005765534913516977, 'mean_word_length': 4.891823899371069, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1065049', 'n_tokens_mistral': 2085, 'n_tokens_neox': 1942, 'n_words': 548}