α : Type u_1
β : Type ?u.22476
γ : Type ?u.22479
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - (↑n - 1)))
α : Type u_1
β : Type ?u.22476
γ : Type ?u.22479
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[Iio ↑n] ↑n) (𝓝 1)
rw [← sub_sub_cancel (n : α) 1]
α : Type u_1
β : Type ?u.22476
γ : Type ?u.22479
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x => ↑⌊x⌋) (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - 1))
α : Type u_1
β : Type ?u.22476
γ : Type ?u.22479
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - (↑n - 1)))
refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_
no goals
α : Type u_1
β : Type ?u.22476
γ : Type ?u.22479
inst✝⁴ : LinearOrderedRing α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
inst✝ : TopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun x => ↑⌊x⌋) (𝓝[Iio ↑n] ↑n) (𝓝 (↑n - 1))
exact tendsto_floor_left' n