## Stream: math-comp analysis

### Topic: Naive question about near

#### Laurent Théry (Jun 03 2021 at 08:38):

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: Feb 09 2023 at 03:06 UTC