In a recent proof I have seen this theorem

```
Lemma near_in_interval (R : realType) (a b : R1) :
{in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
```

while translating in term of `near`

, I get the following theorem that I mananed to prove using `ball_split`

```
Lemma near_lift (R : realType) (P : R -> Prop) (x : R1) :
(\forall y \near x, P y) -> \forall y \near x, \forall z \near y, P z.
```

I am a bit surprised that this not a theorem in the library, so I wonder if this theorem is necessary?

Last updated: Jun 25 2024 at 19:01 UTC