# Zulip Chat Archive

## Stream: new members

### Topic: Limits with positive reals and atBot

#### Daniele Pusceddu (Nov 20 2023 at 09:48):

Hello,

I have been working on a project which uses a "Positive Reals" type and I would now like to

work with simple theorem involving limits, in particular "tending to zero from the right" which I believe I may achieve with `Filter.atBot`

. But after browsing around the Mathlib docs for a while, I believe I am stuck. I am here to humbly ask for suggestions in how to prove theorems similar to the ones in the mwe below. Thank you.

```
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Order.Monotone.Basic
abbrev PReal := { r : ℝ // 0 < r}
notation "ℝ+" => PReal
theorem test1:
Filter.Tendsto (fun (x: ℝ+) => 1 + x) Filter.atBot (nhds 1)
:= by sorry
-- Additionally "With the limit of f for x leading to 0 from the right being defined"
-- I know `lim` is not recommended but I didn't know how else to state this
theorem test2 (f: ℝ+ → ℝ+) (h1: StrictMono f) (x: ℝ+):
limUnder Filter.atBot f < f x
:= by sorry
```

#### Patrick Massot (Nov 20 2023 at 14:18):

The `ℝ+`

notation is really very ambiguous. It could just as well refer to `NNReal`

.

#### Patrick Massot (Nov 20 2023 at 14:19):

My first advice is to reconsider whether you really really want this instead of working with reals.

#### Daniele Pusceddu (Nov 20 2023 at 14:25):

Patrick Massot said:

My first advice is to reconsider whether you really really want this instead of working with reals.

I invested a bit too much in it already to revert back to reals.

#### Patrick Massot (Nov 20 2023 at 14:57):

Here something you can do (but it shows the pain you inflict on yourself with working with PReal):

```
import Mathlib.Topology.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Order.Filter.AtTopBot
import Mathlib.Order.Monotone.Basic
abbrev PReal := { r : ℝ // 0 < r}
notation "ℝ>0" => PReal
open Filter Topology
theorem test1: Tendsto (fun x: ℝ>0 => 1 + x) atBot (𝓝 1) := by
set i : ℝ>0 → ℝ := fun x ↦ x
set f : ℝ>0 → ℝ>0 := fun x ↦ 1+x
set g : ℝ → ℝ := fun x ↦ 1+x
have hg : Tendsto g (𝓝[>] 0) (𝓝 1) := by
apply tendsto_nhdsWithin_of_tendsto_nhds
have : Continuous (fun x : ℝ ↦ 1 + x) := by continuity
convert this.continuousAt.tendsto ; ring
have : i ∘ f = g ∘ i := by ext x; rfl
rw [tendsto_subtype_rng, ← comap_coe_Ioi_nhdsWithin_Ioi]
change Tendsto (i ∘ f) (comap i (𝓝[>] 0)) (𝓝 1)
rw [this]
exact hg.comp tendsto_comap
-- Additionally "With the limit of f for x leading to 0 from the right being defined"
-- I know `lim` is not recommended but I didn't know how else to state this
theorem test2 {f : ℝ>0 → ℝ>0} (h1 : StrictMono f) {x y : ℝ>0} {hf : Tendsto f atBot (𝓝 y)} :
y < f x := by
sorry
```

#### Patrick Massot (Nov 20 2023 at 14:58):

I also took the opportunity to reformat your code to something more standard. You can clear extract a more general lemma here.

#### Daniele Pusceddu (Nov 20 2023 at 15:12):

Patrick Massot said:

I also took the opportunity to reformat your code to something more standard. You can clear extract a more general lemma here.

Thank you very much, seeing this helps a lot already.

Last updated: Dec 20 2023 at 11:08 UTC