tendsto cofinite atTop

Stream: maths

[Chris Birkbeck]

Do we have (or this an easy consquece of something we have):

Tendsto (norm ∘ fun (n : ℤ) ↦ (n : ℝ)) cofinite atTop := by sorry

I can't seem to find it and I have a proof but its ugly and I expect I am just not using the right thing.

(Oops I just noticed I posted this in the wrong stream, I meant to use Is there code for X? sorry)

[Aaron Liu]

import Mathlib


open Filter

theorem tendsto_intCast_atBot_atBot {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] :
    Tendsto ((↑) : ℤ → R) atBot atBot :=
  tendsto_intCast_atBot_iff.2 tendsto_id

lemma tendsto_norm_atBot_atTop : Tendsto (norm : ℝ → ℝ) atBot atTop := tendsto_abs_atBot_atTop


example : Tendsto (norm ∘ fun (n : ℤ) ↦ (n : ℝ)) cofinite atTop := by
  rw [Int.cofinite_eq]
  apply Filter.Tendsto.sup
  · exact tendsto_norm_atBot_atTop.comp tendsto_intCast_atBot_atBot
  · exact tendsto_norm_atTop_atTop.comp tendsto_intCast_atTop_atTop

[Anatole Dedecker]

I would suggest combining docs#Topology.IsClosedEmbedding.tendsto_cocompact, docs#Filter.cocompact_eq_cofinite, and docs#tendsto_norm_cocompact_atTop

[Anatole Dedecker]

(This gives a proof that applies to any closed and discrete subset of a finite-dimensional real vector space)

[Anatole Dedecker]

(And of course we have docs#Int.isClosedEmbedding_coe_real)

[Chris Birkbeck]

Ah thanks, both of those a nicer than what I was doing.

[Jireh Loreaux]

I think the easiest approach is docs#tendsto_norm_atTop_iff_cobounded with docs#tendsto_intCast_atBot_sup_atTop_cobounded and docs#Int.cofinite_eq

[Jireh Loreaux]

But Anatole's is more general.