α : Type u
β : Type v
γ : Type w
⊢ Tendsto (fun y => dist (↑y) 0) cofinite atTop
α : Type u
β : Type v
γ : Type w
⊢ Tendsto Int.cast cofinite (cocompact ℝ)
refine' tendsto_cocompact_of_tendsto_dist_comp_atTop (0 : ℝ) _
α : Type u
β : Type v
γ : Type w
⊢ ∀ (b : ℝ), Set.Finite {x | ↑x ∈ ball 0 b}
α : Type u
β : Type v
γ : Type w
⊢ Tendsto (fun y => dist (↑y) 0) cofinite atTop
simp only [Filter.tendsto_atTop, eventually_cofinite, not_le, ← mem_ball]
α : Type u
β : Type v
γ : Type w
⊢ ∀ (r : ℝ), Set.Finite (Int.cast ⁻¹' ball 0 r)
α : Type u
β : Type v
γ : Type w
⊢ ∀ (b : ℝ), Set.Finite {x | ↑x ∈ ball 0 b}
change ∀ r : ℝ, (Int.cast ⁻¹' ball (0 : ℝ) r).Finite
no goals
α : Type u
β : Type v
γ : Type w
⊢ ∀ (r : ℝ), Set.Finite (Int.cast ⁻¹' ball 0 r)
simp [Real.ball_eq_Ioo, Set.finite_Ioo]