Laurent Théry (Jun 04 2021 at 09:24): 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 xwhat 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