mathlib documentation

topology.algebra.floor_ring

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} [linear_ordered_ring α] [floor_ring α] [topological_space α] {β : Type u_2} {γ : Type u_3} [order_topology α] [topological_add_group α] [topological_space β] [topological_space γ] {f : β → α → γ} :
continuous_on (function.uncurry f) (set.univ.prod (set.Icc 0 1))(∀ (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 : α → β} :
continuous_on f (set.Icc 0 1)f 0 = f 1continuous (f fract)