I have another naive question relating to near : classically we have `~(forall x, P x) = exists x, ~ P x`

what is the equivalent for `~(\forall y \near x, P y)`

Laurent Théry said:

I have another naive question relation near, classically we have

`~(forall x, P x) = exists x, ~ P x`

what is the equalivalent for`~(\forall y \near x, P y)`

Good question, ... in the case of an ultrafilter `F`

the answer would be `~ \forall y \near F, P y = \forall y \near F, ~ P y`

, but the filter of neighborhoods `nbhs x`

is not an ultrafilter unless `x`

is isolated (e.g. if your topology is discrete)

otherwise you have `~ \forall y \near x, P y = forall N, nbhs x N -> exists2 y, N y & ~ P y`

... I don't know if there is a better way to phrase it...

Maybe a skolemization + massaging is even better:

```
~ \forall y \near F, P y = exists2 pick : set X -> X, forall N, ~ P (pick N) & forall N, nbhs x N -> N (pick N)`
```

Last updated: Jun 25 2024 at 19:01 UTC