Stream: math-comp analysis

Topic: not forall near


view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip 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: Aug 11 2022 at 02:03 UTC