## Stream: math-comp analysis

### Topic: not forall near

#### Laurent Théry (Jun 04 2021 at 09:24):

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)`

#### Cyril Cohen (Jun 04 2021 at 09:40):

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)

#### Cyril Cohen (Jun 04 2021 at 09:44):

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...

#### Cyril Cohen (Jun 04 2021 at 09:47):

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