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 : ℤ) :
theorem
tendsto_ceil_left'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
theorem
tendsto_floor_right
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
theorem
tendsto_ceil_left
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
(n : ℤ) :
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
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 : ℤ) :
theorem
tendsto_fract_left
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
theorem
tendsto_fract_right'
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(n : ℤ) :
theorem
tendsto_fract_right
{α : Type u_1}
[linear_ordered_ring α]
[floor_ring α]
[topological_space α]
[order_closed_topology α]
[topological_add_group α]
(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 (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) :
continuous (f ∘ fract)