On continue dans la s\u00e9rie des espaces topologiques avec un exercice sur les axiomes de s\u00e9paration :<\/p>\n\n\n\n
Soit \\((X, T )\\) un espace topologique.
Montrer que les conditions suivantes sont \u00e9quivalentes :
(i) \\(\\forall x, y \\in X, x \\neq y, \\exists V \\text{voisinage de}x, y \\notin V .\\)
(ii) \\(\\forall x \\in X, {x} ferm\u00e9.\\)
(iii) \\(\\forall x \\in X, {V ; V \\text{voisinage de }x} = {x}.\\)
Soit \\((X, T )\\) ainsi et \\(A \\subset X\\) tel que \\(\\overline{A} \\neq A\\). Montrer que si \\(x \\in \\overline{A}\\backslash A\\), tout voisinage de \\(x\\) coupe \\(\\)A en une infinit\u00e9 de points.<\/p><\/blockquote>\n\n\n\nAppart\u00e9 sur la s\u00e9paration<\/h2>\n\n\n\n
Cet exercice m’a donn\u00e9 l’occasion de d\u00e9couvrir le concept de s\u00e9paration en topologie que je ne connaissais que tr\u00e8s vaguement. L’id\u00e9e derri\u00e8re la s\u00e9paration est de caract\u00e9riser le niveau d’ \u00ab\u00a0ind\u00e9pendance\u00a0\u00bb des voisinages de deux points distincts. Plus exactement, on distingue 3 niveaux de s\u00e9parations not\u00e9s T0, T1 et T2:<\/p>\n\n\n\n
- T0 signifie que si on prend deux points distincts, on a au moins un voisinage de l’un qui ne contient pas l’autre,<\/li>
- T1 signifie que si on prend deux points distincts, chacun a au moins un voisinage ne contenant pas l’autre,<\/li>
- Enfin T2 est le niveau au dessus : si on prend deux points distincts, on a au moins un couple de voisinage respectif qui sont disjoints.<\/li><\/ul>\n\n\n\n
La plupart des espaces usuels (les r\u00e9els, complexes, espaces vectoriels…) sont T2. Parmi les espaces qui ne sont pas s\u00e9par\u00e9s il y a les topologies grossi\u00e8res (ie l’ensemble entier et l’ensemble vide). J’avoue que je ne connais pas la motivation derri\u00e8re les niveaux T0 et T1 et je n’ai pas d’exemples d’espace v\u00e9rifiant ces niveaux mais pas les suivants.<\/p>\n\n\n\n
Le trio d’\u00e9quivalence est semble-t-il une propri\u00e9t\u00e9 fondamentale des axiomes de s\u00e9paration puisqu’il est directement pr\u00e9sent\u00e9 comme propri\u00e9t\u00e9 dans mon livre de topologie, qui le d\u00e9montre de bas en haut. J’ai essay\u00e9 d’effectuer la d\u00e9monstration en Coq de haut en bas mais je me suis retrouv\u00e9 bloquer en cherchant \u00e0 passer de (ii) \u00e0 (iii) ; ayant ensuite d\u00e9cid\u00e9 qu’il \u00e9tait peut-\u00eatre plus sage de suivre une voie connue, j’ai finalement opt\u00e9 pour la d\u00e9monstration de bas en haut. Il s’av\u00e8re que le passage de (iii) \u00e0 (ii) est aussi compliqu\u00e9 et que dans les autres cas les preuves sont plus ou moins des \u00ab\u00a0miroirs\u00a0\u00bb de celles que j’avais faite dans ma premi\u00e8re tentative, j’imagine ais\u00e9ment qu’il est malgr\u00e9 tout possible d’effectuer la preuve dans n’importe quel sens.<\/p>\n\n\n\n
Pr\u00e9alable<\/h2>\n\n\n\n
Une propri\u00e9t\u00e9 particuli\u00e8rement utile pour cette exercice est la caract\u00e9risation de l’adh\u00e9rence d’un ensemble, appel\u00e9 closure_impl_meets_every_open_neighborhood dans coq-topology : un point est dans l’adh\u00e9rence d’un ensemble si tous ses voisinages rencontrent cet ensemble, ou dit autrement si l’intersection de ses voisinages avec cet ensemble n’est jamais vide.<\/p>\n\n\n\n
Du point de vue plus pratique, on continue \u00e0 utiliser quelques astuces qui simplifient la vie sur le long terme : on d\u00e9finit une tactic ensemble_proof_intro pour automatiquement nous fournir les 2 inclusions de l’\u00e9galit\u00e9 de l’ensemble \u00e0 prouver, on se sert d’inversion plut\u00f4t que de destruct, et on nomme autant que possible les hypoth\u00e8ses\/variables pour faciliter la lecture.<\/p>\n\n\n\n
A noter qu’\u00e0 un moment j’ai eu besoin de d\u00e9finir un axiome sur la d\u00e9cidabilit\u00e9 sur l’\u00e9galit\u00e9 de 2 \u00e9l\u00e9ments d’un ensemble. Par d\u00e9faut si deux \u00e9l\u00e9ments d’un ensemble ne sont pas \u00e9gaux, Coq ne d\u00e9duit pas automatiquement qu’ils sont diff\u00e9rents ; en effet la logique constructive sur laquelle est bas\u00e9e Coq se passe de l’axiome du tiers exclu qui stipule qu’une propri\u00e9t\u00e9 (comme ici l’\u00e9galit\u00e9) est vraie ou sa n\u00e9gation est vraie. Il faut donc manuellement indiqu\u00e9 que dans notre cas, c’est vrai.<\/p>\n\n\n\n
Trio d’\u00e9quivalence<\/h2>\n\n\n\n
On commence par les imports de circonstances et l’\u00e9criture des propri\u00e9t\u00e9s :<\/p>\n\n\n
\nFrom Topology Require Import TopologicalSpaces.\nFrom Topology Require Import InteriorsClosures.\nFrom Topology Require Import Neighborhoods.\nRequire Import Decidable.\n\nDefinition P1 (X:TopologicalSpace) :=\n forall x y:point_set X, not (x = y) -> exists N, neighborhood N x \/\\ not (In N y).\n\nDefinition P2 (X:TopologicalSpace) :=\n forall x:point_set X, closed (Singleton x).\n\nDefinition P3 (X:TopologicalSpace) :=\n forall x:point_set X, FamilyIntersection [V:Ensemble (point_set X) | neighborhood V x] = Singleton x.\n\nLtac ensemble_proof_intro:=apply Extensionality_Ensembles; unfold Same_set; split.\n<\/pre><\/div>\n\n\nOn aura \u00e9galement besoin de montrer que si un singleton est contenu dans un autre, alors leur \u00e9l\u00e9ment est \u00e9gal :<\/p>\n\n\n
\nTheorem Singleton_Inclusion (T:Type): forall x y:T, Included (Singleton x) (Singleton y) -> x = y.\nProof.\n intros.\n unfold Included in H. symmetry. apply Singleton_inv. apply H. eauto with sets.\nQed.\n\n<\/pre><\/div>\n\n\nOn commence ensuite par l’implication la plus compliqu\u00e9, P3 vers P2 :<\/p>\n\n\n
\nTheorem P3_implies_P2 {X:TopologicalSpace}:\n P3 X -> P2 X.\nProof.\n unfold P3. unfold P2.\n \n intros P3 x0.\n<\/pre><\/div>\n\n\nLa strat\u00e9gie pour montrer que le singleton x est ferm\u00e9, est de montrer qu’il est \u00e9gal \u00e0 son adh\u00e9rence. Cette strat\u00e9gie part de l’intuition que l’\u00e9criture de l’ensemble des voisinages est proche d’une intersection en ensemble de ferm\u00e9 contenant un ensemble.<\/p>\n\n\n
\n assert (Included (closure (Singleton x0)) (Singleton x0)).\n\n unfold Included.\n intros x xInClosure.\n<\/pre><\/div>\n\n\nOn va se servir de la propri\u00e9t\u00e9 sur la caract\u00e9risation des adh\u00e9rences. Quand on regarde les hypoth\u00e8ses de cette propri\u00e9t\u00e9, on voit qu’il va falloir trouver un ouvert, qui contient x, et on en d\u00e9duira que x0 est dans V (car l’intersection du singleton x0 et V est non vide).<\/p>\n\n\n
\npose (tmp2:=closure_impl_meets_every_open_neighborhood _ (Singleton x0) x xInClosure).\n\n assert (forall V, open_neighborhood V x -> Inhabited (Intersection (Singleton x0) V)).\n intros V VNeighbor. inversion VNeighbor. unfold open_neighborhood in VNeighbor.\n apply tmp2. \n assumption. assumption.\n assert(forall V, open_neighborhood V x -> In V x0).\n intros. pose (tmp3:=H V H0). inversion tmp3. inversion H1. inversion H2. subst. assumption.\n<\/pre><\/div>\n\n\nPour rappel, on cherche \u00e0 montrer ici que x est dans le singleton x0, ie que x = x0. Pour l’instant on n’a pas encore utilis\u00e9 l’hypoth\u00e8se P3. Pour se simplifier la vie on peut remarquer qu’on peut se servir des voisinages ouverts plut\u00f4t que des voisinages quelconques :<\/p>\n\n\n
\n\n assert( forall x : point_set X, FamilyIntersection [V : Ensemble (point_set X) | neighborhood V x] =\n FamilyIntersection [V : Ensemble (point_set X) | open_neighborhood V x]).\n {\n intros x1. ensemble_proof_intro.\n - intros S SinInters. inversion SinInters.\n constructor. intros. apply H1. inversion H3. constructor. apply open_neighborhood_is_neighborhood. apply H4.\n - intros y yinIntersOpen. inversion yinIntersOpen.\n constructor. intros S SInInters. inversion SInInters as [[S' [OpenS' S'InS]]].\n refine (S'InS _ _). apply H1. split. assumption.\n }\n<\/pre><\/div>\n\n\nMuni de ce r\u00e9sultat on peut prouver l’\u00e9galit\u00e9:<\/p>\n\n\n
\n\n assert(Included (Singleton x0) (Singleton x)).\n unfold Included. intros y yisx0. inversion yisx0.\n rewrite <- (P3 x).\n rewrite (H1 x).\n constructor.\n intros. inversion H3. subst. eauto.\n<\/pre><\/div>\n\n\net donc l’inclusion inverse :<\/p>\n\n\n
\n apply Singleton_intro.\n refine (Singleton_Inclusion _ _ _ _). assumption.\n<\/pre><\/div>\n\n\nLa suite est relativement directe:<\/p>\n\n\n
\n\n assert (closure (Singleton x0) = Singleton x0).\n ensemble_proof_intro.\n apply H. apply closure_inflationary.\n rewrite <- H0. apply closure_closed.\nQed.\n<\/pre><\/div>\n\n\nL’inclusion P2 vers P1 est plus simple:<\/p>\n\n\n
\nTheorem P2_implies_P1 {X:TopologicalSpace}:\n P2 X -> P1 X.\nProof.\n unfold P1, P2.\n intros P2 x y xNeqy.\n unfold closed in P2.\n\n exists (Complement (Singleton y)). split.\n unfold neighborhood. exists (Complement (Singleton y)). split. unfold open_neighborhood. split. apply (P2 y).\n unfold Complement. unfold not. unfold In. intros. destruct xNeqy. inversion H. trivial.\n eauto with sets.\n eauto with sets.\nQed.\n<\/pre><\/div>\n\n\nCelle de P1 vers P3 n’est pas beaucoup plus compliqu\u00e9, mais n\u00e9cessite quand m\u00eame la d\u00e9cidabilit\u00e9 dont on a pr\u00e9alablement parl\u00e9, pour faire une disjonction de cas :<\/p>\n\n\n
\nTheorem P1_implies_P3 {X:TopologicalSpace}:\n P1 X -> P3 X.\nProof.\n unfold P1. unfold P3.\n intros P1 x0.\n ensemble_proof_intro.\n - unfold Included. intros x xInIntersNeigh.\n destruct (decT X x0 x).\n + eauto with sets.\n + inversion xInIntersNeigh. destruct (P1 x0 x H). inversion H2. pose (tmp:= H0 x2). autounfold with sets in tmp.\n assert([V : Ensemble (point_set X) | neighborhood V x0] x2).\n constructor. assumption.\n apply tmp in H5. destruct (H4 H5).\n - unfold Included. intros x xIsx0.\n inversion xIsx0.\n constructor. intros. inversion H0. inversion H1. inversion H2. unfold Included in H4. apply H4. inversion H3. assumption.\nQed.\n<\/pre><\/div>\n\n\nSeconde propri\u00e9t\u00e9<\/h2>\n\n\n\n
Alors l\u00e0 c’est vraiment costaud \u00e0 d\u00e9montrer, la faute \u00e0 la d\u00e9monstration de l’infinit\u00e9. Coq dispose de quelques r\u00e9sultats sur les ensembles infinis, mais malheureusement peu nombreux et que nous n’utiliserons donc pas.
En revanche il est beaucoup plus simple de travailler sur les ensembles finis, on va donc proc\u00e9der par l’absurde.<\/p>\n\n\n\nEn particulier une propri\u00e9t\u00e9 des ouverts qui est vraie dans le cas des ensembles finies mais qui ne l’est plus dans les ensembles infinis est la stabilit\u00e9 par intersection. On va donc prouver cette propri\u00e9t\u00e9, par r\u00e9cursion sur la taille de l’ensemble :<\/p>\n\n\n
\nTheorem intersection_finite (X:TopologicalSpace):\n forall F:Family (point_set X), Finite _ F \/\\ (forall S, In F S -> open S) -> open (FamilyIntersection F).\nProof.\n intros F [F_Finite F_Set_Of_Opens].\n apply finite_cardinal in F_Finite.\n destruct F_Finite as [n cardFn].\n generalize dependent F.\n induction n ; intros F cardFn F_Set_Of_Opens.\n - inversion cardFn. Search FamilyIntersection. rewrite empty_family_intersection.\n Print TopologicalSpace. apply open_full.\n - inversion cardFn. pose (tmp:= IHn A H0).\n assert(FamilyIntersection (Add A x) = Intersection (FamilyIntersection A) x).\n ensemble_proof_intro; unfold Included; intros x0.\n + intros x0InIntersAx.\n inversion x0InIntersAx.\n constructor.\n * constructor. eauto with sets.\n * eauto with sets.\n + intros x0InInters. inversion x0InInters. inversion H3. constructor. unfold Add.\n intros. inversion H8.\n * eauto with sets.\n * inversion H9. subst. eauto with sets.\n\n + rewrite H3. apply open_intersection2.\n\n * apply tmp. intros. apply F_Set_Of_Opens. Search Add.\n unfold Add in H1. rewrite <- H1. eauto with sets.\n * apply F_Set_Of_Opens. rewrite <- H1. unfold Add. eauto with sets.\nQed. \n<\/pre><\/div>\n\n\nUn autre r\u00e9sultat qui m’a \u00e9t\u00e9 utile est que l’\u00e9galit\u00e9 est conserv\u00e9e par passage au compl\u00e9ment :<\/p>\n\n\n
\n\nTheorem Complement_inv (X:Type) : forall (S1 S2: Ensemble X), Complement S1 = Complement S2 -> S1 = S2.\nProof.\n intros. ensemble_proof_intro; rewrite <- Complement_Complement with (A:=S1); rewrite <- Complement_Complement with (A:=S2); apply complement_inclusion; rewrite H; eauto with sets.\nQed.\n<\/pre><\/div>\n\n\nOn peut ensuite passer \u00e0 la d\u00e9monstration en elle-m\u00eame :<\/p>\n\n\n
\nTheorem part2 (X:TopologicalSpace): P2 X -> forall A: Ensemble (point_set X), forall x, In (Setminus (closure A) A) x -> forall N, neighborhood N x -> not (Finite _ (Intersection N A)).\nProof.\n intros P2 A x0 x0inclAminA.\n unfold Top.P2 in P2.\n destruct x0inclAminA as [x0InClA x0NotInA].\n intros N [O [[OpenO x0inO] OInN]].\n \n pose (tmp:=closure_impl_meets_every_open_neighborhood _ A x0 x0InClA).\n\n unfold not. intros NInterAFinite.\n \n remember (fun E => exists x, In (Intersection N A) x \/\\ E = Complement (Singleton x)) as SetOfElems.\n (**pose (tmp3:=intersection_finite _ SetOfElems).**)\n assert(Finite _ SetOfElems).\n generalize dependent SetOfElems.\n induction NInterAFinite; intros.\n - assert (SetOfElems = Empty_set). rewrite HeqSetOfElems. ensemble_proof_intro.\n + unfold Included. intros. unfold In in H. destruct H. destruct H. destruct H.\n + eauto with sets.\n + rewrite H. eauto with sets.\n\n\n - assert (SetOfElems = Add (fun E : Ensemble (point_set X) => exists x0 : point_set X, In A0 x0 \/\\ E = Complement (Singleton x0)) (Complement (Singleton x))).\n ensemble_proof_intro ; unfold Included; rewrite HeqSetOfElems.\n + intros. inversion H0. inversion H1. unfold In. inversion H2 as [x2InA0|]. \n * left. exists x2. split. assumption. assumption.\n * right. inversion H4. subst. eauto with sets.\n + intros. unfold In. inversion H0.\n * inversion H1. inversion H3. exists x3. split. left. assumption. assumption.\n * exists x. inversion H1. split. right. eauto with sets. trivial.\n\n\n + rewrite H0. constructor.\n * remember (fun E : Ensemble (point_set X) => exists x1 : point_set X, In A0 x1 \/\\ E = Complement (Singleton x1)) as P0.\n apply IHNInterAFinite. trivial.\n * unfold In. unfold not. intros. inversion H1. inversion H2.\n apply Complement_inv in H4. \n apply Singleton_equal in H4. subst. destruct (H H3).\n \n \n - remember (FamilyIntersection SetOfElems) as ContraGen.\n assert (open ContraGen).\n rewrite HeqContraGen.\n apply intersection_finite. split.\n + assumption.\n + intros S SInSetOfElems. rewrite HeqSetOfElems in SInSetOfElems. unfold In in SInSetOfElems. inversion SInSetOfElems.\n inversion H0. rewrite H2. refine (P2 _).\n + pose (contra:= tmp (Intersection ContraGen O) (open_intersection2 ContraGen O H0 OpenO)).\n assert (In (Intersection ContraGen O) x0).\n rewrite HeqContraGen.\n constructor. constructor. rewrite HeqSetOfElems. intros. unfold In in H1. inversion H1. inversion H2. rewrite H4. Search Intersection. apply Intersection_decreases_r in H3. unfold In. unfold Complement. unfold not. intros. inversion H5. subst. contradiction.\n assumption.\n\n apply contra in H1. inversion H1. inversion H2. inversion H4. rewrite HeqContraGen in H6. rewrite HeqSetOfElems in H6. unfold In in H6. inversion H6. pose (contra2:= H9 (Complement (Singleton x))). unfold In in contra2.\n assert(exists x0 : point_set X, Intersection N A x0 \/\\ Complement (Singleton x) = Complement (Singleton x0)). exists x. split. constructor.\n eauto with sets. eauto with sets. trivial. apply contra2 in H11. destruct H11. constructor.\nQed.\n<\/pre><\/div>","protected":false},"excerpt":{"rendered":"On continue dans la s\u00e9rie des espaces topologiques avec un exercice sur les axiomes de s\u00e9paration : Soit un espace topologique. Montrer que les conditions suivantes sont \u00e9quivalentes : (i) (ii) (iii) Soit ainsi et tel que . Montrer que si , tout voisinage de coupe A en une infinit\u00e9 de points. Appart\u00e9 sur la […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/111"}],"collection":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=111"}],"version-history":[{"count":11,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/111\/revisions"}],"predecessor-version":[{"id":122,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/111\/revisions\/122"}],"wp:attachment":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=111"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=111"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=111"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}