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 #
tendsto_floor_at_top,tendsto_floor_at_bot,tendsto_ceil_at_top,tendsto_ceil_at_bot:int.floorandint.ceiltend to +-∞ in +-∞.continuous_on_floor:int.flooris continuous onIco n (n + 1), because constant.continuous_on_ceil:int.ceilis continuous onIoc n (n + 1), because constant.continuous_on_fract:int.fractis continuous onIco n (n + 1).continuous_on.comp_fract: Precomposing a continuous function satisfyingf 0 = f 1withint.fractyields another continuous function.
theorem
continuous_on_floor
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
(n : ℤ) :
theorem
continuous_on_ceil
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
(n : ℤ) :
theorem
tendsto_floor_right'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌊x⌋) (nhds_within ↑n (set.Ici ↑n)) (nhds ↑n)
theorem
tendsto_ceil_left'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌈x⌉) (nhds_within ↑n (set.Iic ↑n)) (nhds ↑n)
theorem
tendsto_floor_right
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌊x⌋) (nhds_within ↑n (set.Ici ↑n)) (nhds_within ↑n (set.Ici ↑n))
theorem
tendsto_ceil_left
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌈x⌉) (nhds_within ↑n (set.Iic ↑n)) (nhds_within ↑n (set.Iic ↑n))
theorem
tendsto_floor_left
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌊x⌋) (nhds_within ↑n (set.Iio ↑n)) (nhds_within (↑n - 1) (set.Iic (↑n - 1)))
theorem
tendsto_ceil_right
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
filter.tendsto (λ (x : α), ↑⌈x⌉) (nhds_within ↑n (set.Ioi ↑n)) (nhds_within (↑n + 1) (set.Ici (↑n + 1)))
theorem
tendsto_floor_left'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
theorem
tendsto_ceil_right'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
theorem
continuous_on_fract
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[topological_add_group α]
(n : ℤ) :
theorem
tendsto_fract_left'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
filter.tendsto int.fract (nhds_within ↑n (set.Iio ↑n)) (nhds 1)
theorem
tendsto_fract_left
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
filter.tendsto int.fract (nhds_within ↑n (set.Iio ↑n)) (nhds_within 1 (set.Iio 1))
theorem
tendsto_fract_right'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
filter.tendsto int.fract (nhds_within ↑n (set.Ici ↑n)) (nhds 0)
theorem
tendsto_fract_right
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
filter.tendsto int.fract (nhds_within ↑n (set.Ici ↑n)) (nhds_within 0 (set.Ici 0))
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) :
continuous (f ∘ int.fract)
A special case of continuous_on.comp_fract.