Laurent Théry (Jun 03 2021 at 08:38): 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: Oct 13 2024 at 01:02 UTC