Two simple calculus lemmas

Stream: mathlib4

[Michael Stoll]

I need the following two results, but find it hard to produce elegant proofs:

import Mathlib

open Topology Filter

lemma foo {f : ℝ → ℝ} {x : ℝ} (hf : ContinuousAt f x) :
    ∃ C : ℝ, ∀ᶠ (y : ℝ) in (𝓝 x), C ≤ f y := by
  sorry

lemma bar {a : ℝ} (ha : a > 0) (b : ℝ) :
    Tendsto (fun x : ℝ ↦ a / (x - b)) (𝓝[>] b) atTop := by
  sorry

Any pointers?

[Alex Kontorovich]

For the first one, won't something like use f x - 1 and then eventually_lt_of_tendsto_lt work?

[Matt Diamond]

lemma foo {f : ℝ → ℝ} {x : ℝ} (hf : ContinuousAt f x) :
    ∃ C : ℝ, ∀ᶠ (y : ℝ) in (𝓝 x), C ≤ f y :=
⟨f x - 1, eventually_ge_of_tendsto_gt (by simp) hf.tendsto⟩

[Alex Kontorovich]

lemma foo {f : ℝ → ℝ} {x : ℝ} (hf : ContinuousAt f x) :
    ∃ C : ℝ, ∀ᶠ (y : ℝ) in (𝓝 x), C ≤ f y := by
  exact ⟨f x - 1, eventually_ge_of_tendsto_gt (by linarith) hf⟩

[Alex Kontorovich]

Second one should use tendsto_inv_zero_atTop. (inv is better than $1/x$...)

[Michael Stoll]

Thanks! This helps.

[Michael Stoll]

And is there a better way of showing Tendsto (fun x ↦ x - 1) (𝓝[>] 1) (𝓝[>] 0) than going via epsilons and deltas? apply? is decidedly unhelpful in this part of the library...

[Jireh Loreaux]

You'll want to use docs#ContinuousWithinAt.tendsto_nhdsWithin_image

[Jireh Loreaux]

Note that 𝓝[>] 1 is just notation for nhdsWithin 1 (Set.Ioi 1)