Stream: math-comp analysis

Topic: Naive question about near

view this post on Zulip 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: Aug 11 2022 at 02:03 UTC