Introduce T_0 and T_1 spaces and prove T_1 -> T0.

[vlj]

This PR adds T0 and T1 spaces definitions, proof that singletons in T1 space are closed, and that T1 -> T0.

I introduced 2 lemmas in classical_sets to make easy to work with [set~ x] : setC_set1C and setC_subset_set1C. I'm not really sure about the naming convention:

• setC_set1C isn't technically an elimination so it can't be named set1C, but it's very close... I wonder if it's not better to have a Lemma proving "[y | y != x] = [set~ x]".
• setC_subset_set1C is involving a subset of set1C, but I don't know how to phrase it correctly. I'm also not sure my proof is optimal.
  For "T_1_singleton_closed" I have an extra "have xNeqY:" step, I don't know if it can't be more elegantly derived using the setC_set1C lemma.

[vlj]

Actually I used setC1E since it makes the other proof cleaner.

[affeldt-aist]

This PR adds T0 and T1 spaces definitions, proof that singletons in T1 space are closed, and that T1 -> T0.

Thank you for your contribution!

I introduced 2 lemmas in classical_sets to make easy to work with [set~ x] : setC_set1C and setC_subset_set1C.
I'm not really sure about the naming convention:

For T_0 and T_1, we should maybe go with full names like we did for hausdorff, otherwise it looks too much
like code identifier.

* setC_subset_set1C is involving a subset of set1C, but I don't know how to phrase it correctly.

I'm also not sure my proof is optimal.

It can be a one-liner, I am not sure about the naming either, I would propose to name it on the model of
disjoints_subset because it looks like a special case.

[CohenCyril]

FYI

• removed useless setC1E (it is convertible and inE yields the same result)
• removed mem_setC_subset which was a duplicate of setC_subset_set1C
• generalized and renamed the latter to subsetC1
• removed all uses of -in_setE

[affeldt-aist]

Double-checked and comments from the last meeting applied. Ready to merge.