∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (n : ℤ),
  Filter.Tendsto (fun x => ↑⌊x⌋) (nhdsWithin (↑n) (Set.Ici ↑n)) (nhdsWithin (↑n) (Set.Ici ↑n))