Sequential closedness
Let
Proof
Let
be closed, πΉ β π , and π = π β πΉ be sequence in ( π₯ π ) β π = 1 such that πΉ . But since ( π₯ π ) β π₯ β π is an open neighbourhood of π , there exists some π₯ such that π for all π₯ π β π , so π > π for all π₯ π β πΉ , a contradiction. π > π
Main theorem
Let
Proof
The forward direction is given above. For the converse, let
such that for every sequence πΉ β π , ( π₯ π ) β π = 1 implies ( π₯ π ) β π₯ . Suppose π₯ β πΉ is not open in π = π β πΉ Then there exists some π such that for every neighbourhood π¦ β π of π , π¦ . Since π β© πΉ β β is first-countable, we may construct a nested neighbourhood basis π , for which { π π } β π = 1 for all π π β© πΉ β β . One may then construct a sequence π β β such that ( π₯ π ) β π = 1 for all π₯ π β π π β© πΉ . But then π β β , contradicting the requirement that ( π₯ π ) β π¦ β π be sequentially closed. Hence πΉ must be open, whence π is closed. πΉ