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