Alors celui l\u00e0, il est costaud malgr\u00e9 son apparente\nsimplicit\u00e9. Commen\u00e7ons par l\u2019\u00e9nonc\u00e9 :<\/p>\n\n\n\n
Dans un espace topologique, on d\u00e9finit la fronti\u00e8re d\u2019une partie A comme \u00e9tant \\(\\partial A = \\overline{A}\\backslash \\mathring{A}\\). <\/p>
Montrer que \\(
\\partial A =
\\partial (A^c )\\) et que \\(A =
\\partial A \\Leftrightarrow A\\) ferm\u00e9 d\u2019int\u00e9rieur vide. <\/p>
Montrer que \\(
\\partial (\\overline{A})\\) et \\(
\\partial (\\mathring{A})\\) sont toutes deux incluses dans \\(
\\partial A\\), et donner un exemple o\u00f9 ces inclusions sont strictes. <\/p>
Montrer que \\(
\\partial (A \\cup B) \\subset
\\partial A \\cup
\\partial B\\), et que l\u2019inclusion peut-\u00eatre stricte ; montrer qu\u2019il y a \u00e9galit\u00e9 lorsque \\(\\overline{A} \\cup \\overline{B} = \u2205\\) (\u00e9tablir \\(\\mathring{A \\cup B} \\subset \\mathring{A} \\cup \\mathring{B}\\)). <\/p>
Montrer que \\(\\mathring{A \\cup B} = \\mathring{A} \\cup \\mathring{B}\\) reste vrai lorsque \\(
\\partial A \\cap
\\partial B = \u2205\\) (raisonner par l\u2019absurde) <\/p><\/blockquote>\n\n\n\nIl s\u2019agit d\u2019un exercice relativement classique pour un \u00e9tudiant en topologie, qui permet surtout de manipuler les d\u00e9finitions d\u2019int\u00e9rieur et d\u2019adh\u00e9rence et quelques formules sur les ensembles. Oui mais voil\u00e0, la plupart des r\u00e9sultats \u00ab intuitifs \u00bb sur les ensembles ont besoin d\u2019\u00eatre prouv\u00e9, ce qui donne lieu \u00e0 des preuves fastidieuses. Pire, il n\u2019est pas rare de se pr\u00e9cipiter dans de fausses pistes, en substituant une d\u00e9finition de trop. Bref, cet exercice m\u2019a demand\u00e9 mine te rien plusieurs jours \u00e0 effectuer, et surtout \u00e0 passer par la case papier + crayon alors que je m\u2019en \u00e9tais pass\u00e9 jusque l\u00e0. Il est n\u00e9anmoins tr\u00e8s formateur puisqu\u2019il invite \u00e0 chercher des moyens d\u2019abr\u00e9ger l\u2019\u00e9criture de preuve, \u00e0 d\u00e9couper quelques r\u00e9sultats interm\u00e9diaires.<\/p>\n\n\n\n
Quelques pr\u00e9alables<\/h2>\n\n\n\n
On \u00e9vacue d\u00e9j\u00e0 la d\u00e9finition d’une fronti\u00e8re :<\/p>\n\n\n
\nDefinition frontier (X:TopologicalSpace) (A:Ensemble (point_set X)) :=\n Setminus (closure A) (interior A).\n<\/pre><\/div>\n\n\nLa taille de l’exercice est un bon pr\u00e9texte pour s’autoriser \u00e0 essayer les possibilit\u00e9s d’automation que propose Coq. On commence modeste avec une tactique personnalis\u00e9e \u00ab\u00a0ensemble_proof_intro\u00a0\u00bb qui n’est qu’une esp\u00e8ce de macro sur un enchainement qu’on trouve souvent lorsqu’on travaille avec des ensembles : la r\u00e9\u00e9criture en double inclusion et la g\u00e9n\u00e9ration des 2 objectifs associ\u00e9s.<\/p>\n\n\n
\nLtac ensemble_proof_intro:=\n apply Extensionality_Ensembles; unfold Same_set; split.\n<\/pre><\/div>\n\n\nPremier point<\/h2>\n\n\n\n
Muni de ce petit raccourci, le premier r\u00e9sultat est assez direct \u00e0 prouver :<\/p>\n\n\n
\nTheorem frontier_comp (X:TopologicalSpace) (A:Ensemble (point_set X)):\n frontier X A = frontier X (Complement A).\nProof.\n unfold frontier. apply Extensionality_Ensembles. unfold Same_set. split; unfold Included; unfold Setminus in *; rewrite interior_complement; rewrite closure_complement; unfold In in * ;intros; destruct H.\n - split ; unfold Complement.\n + apply H0.\n + unfold not. intros. destruct (H1 H).\n - unfold In. split. Search (Complement). Print Complement. pose (tmp:= (Complement_Complement _ (closure A))). unfold Complement in tmp. rewrite <- tmp. unfold In. unfold Complement in H0. apply H0. apply H.\nQed.\n<\/pre><\/div>\n\n\nEn revanche pour l’\u00e9quivalence j’ai eu beaucoup plus de mal. La tentation est grande de remplacer A par sa d\u00e9finition en terme de fronti\u00e8re partout d\u00e8s le d\u00e9but mais est contre-productive : une fa\u00e7on de prouver est de montrer que si on est dans l’int\u00e9rieur de A on est aussi dans le compl\u00e9mentaire de l’int\u00e9rieur de A.<\/p>\n\n\n\n
Un autre \u00e9cueil, certes moins bloquant, est d’unfolder les Included ce qui va rajouter pas mal de \u00ab\u00a0bruits\u00a0\u00bb dans les hypoth\u00e8ses ; une hypoth\u00e8se de type Included S (interior A) s’est retrouv\u00e9e \u00ab\u00a0dilu\u00e9e\u00a0\u00bb lors de mes premi\u00e8res tentatives et m’a oblig\u00e9 \u00e0 la recr\u00e9er via assert.<\/p>\n\n\n\n
La d\u00e9finition de Setminus est toutefois assez peu pratique \u00e0 utiliser, on va donc utiliser une \u00e9criture interm\u00e9diaire \u00e0 base d’intersection et de compl\u00e9mentaire. Une occasion \u00e9galement d’utiliser la tactic eauto (pour une raison que j’ignore, elle fonctionne beaucoup mieux que la tactique auto). <\/p>\n\n\n\n
D’apr\u00e8s la documentation Coq, cette tactique va essayer d’appliquer la tactique apply (et non des rewrite !) avec des th\u00e9or\u00e8mes group\u00e9es dans une base de donn\u00e9e qui peut \u00eatre \u00e9tendue. En pratique, cette tactique marche bien si on a des hypoth\u00e8ses de type \u00ab\u00a0In S x\u00a0\u00bb dans le contexte et peu de Complement.<\/p>\n\n\n
\nTheorem setminus_as_intersection (X:Type):\n forall A B:Ensemble X, Setminus A B = Intersection A (Complement B).\nProof.\n intros A B.\n ensemble_proof_intro; unfold Setminus; unfold Included; unfold Complement; unfold In; intros; destruct H.\n - constructor ; eauto with sets.\n - split; eauto with sets.\nQed.\n<\/pre><\/div>\n\n\nQuelques mini r\u00e9sultats sur les ensembles qui simplifient la d\u00e9monstration de la seconde partie du premier point. Bien entendu je n’ai pas planifi\u00e9 \u00e0 l’avance, j’ai extrait ces r\u00e9sultats quand le besoin s’en ait fait ressentir.<\/p>\n\n\n
\nTheorem include_intersection (T:Type): forall (S1 S2 S3:Ensemble T), Included S3 (Intersection S1 S2) <-> Included S3 S1 \/\\ Included S3 S2.\nProof.\n intros. split.\n - intros. split ; unfold Included in *; intros; pose (tmp:= H x H0); destruct tmp.\n + apply H1.\n + apply H2.\n - intros. destruct H. unfold Included in *. intros. constructor. apply H. apply H1. apply H0. apply H1.\nQed.\n\nTheorem Empty_set_intersection (T:Type): forall A: Ensemble T, Intersection A (Complement A) = Empty_set.\nProof.\n intros. ensemble_proof_intro.\n - unfold Included. unfold Complement. intros. destruct H. destruct (H0 H).\n - apply Included_Empty.\nQed.\n\nTheorem Intersection_Complement_Empty_set (T:Type): forall S:Ensemble T,\n Intersection S (Complement Empty_set) = S.\nProof.\n intros. ensemble_proof_intro ;autounfold with sets; intros.\n - destruct H. eauto.\n - constructor.\n * eauto.\n * unfold Complement. unfold In. repeat autounfold in *. intros. destruct H0.\nQed.\n<\/pre><\/div>\n\n\nAfin de me faciliter la vie j’ai \u00e9galement cr\u00e9\u00e9 une base de donn\u00e9e de r\u00e9\u00e9criture ne contenant que le th\u00e9or\u00e8me rempla\u00e7ant Setminus par une intersection. L’int\u00e9r\u00eat n’est pas de rendre la preuve automatique (autant \u00e9crire rewrite setminus_as_intersection directement) mais permet surtout d’effectuer plusieurs r\u00e9\u00e9criture en une seule fois (ce qu’on aurait pu faire avec repeat).<\/p>\n\n\n
\nHint Rewrite -> setminus_as_intersection : sets_helper.\n<\/pre><\/div>\n\n\nSur ce voici comment prouver la seconde partie du r\u00e9sultat :<\/p>\n\n\n
\nTheorem frontier_equiv (X:TopologicalSpace) (A:Ensemble (point_set X)):\n A = frontier X A <-> closed A \/\\ (interior A = Empty_set).\nProof.\n autounfold in *. autorewrite with sets_helper. split.\n - intro HypFrontierEgalite. split.\n + rewrite HypFrontierEgalite. apply closed_intersection2; try (rewrite <- closure_complement); apply closure_closed.\n + ensemble_proof_intro.\n * unfold Included. intros x xInInteriorA. destruct xInInteriorA as [S x0 HypS x0InS]. destruct HypS. destruct H as [openS SInA].\n assert (Included S (interior A)).\n unfold Included. intros. unfold interior. eapply family_union_intro with (S:=S). split. split. apply openS. apply SInA. apply H.\n\n assert (Included S (Complement (interior A))).\n rewrite HypFrontierEgalite in SInA. rewrite include_intersection in SInA. destruct SInA. apply H1.\n\n assert (Included S (Intersection (interior A) (Complement (interior A)))).\n unfold Included. intros. constructor. apply (H x H1). apply (H0 x H1).\n\n rewrite Empty_set_intersection in H1. destruct (H1 x0 x0InS).\n * apply Included_Empty.\n - intros [HypClosed HypInteriorEmpty]. rewrite HypInteriorEmpty.\n autorewrite with sets_helper.\n ensemble_proof_intro.\n + apply closure_inflationary.\n + rewrite closure_fixes_closed. eauto with sets. assumption.\nQed.\n<\/pre><\/div>\n\n\nSecond point<\/h2>\n\n\n\n
Les inclusions des fronti\u00e8res des int\u00e9rieurs et des adh\u00e9rences ne sont pas tr\u00e8s compliqu\u00e9es \u00e0 d\u00e9montrer, il s’agit surtout d’utiliser les th\u00e9or\u00e8mes de croissance et d’inflation\/d\u00e9flation de ces objets math\u00e9matiques :<\/p>\n\n\n
\nTheorem incl_frontier (X:TopologicalSpace) (A:Ensemble (point_set X)):\n Included (frontier X (interior A)) (frontier X A).\nProof.\n autounfold. autorewrite with sets_helper.\n unfold Included. \n intros _ [x xInClosureInteriorA xInComplementClosureInteriorA].\n autounfold with sets.\n constructor.\n - refine (closure_increasing _ _ _ x xInClosureInteriorA).\n apply interior_deflationary.\n - refine (complement_inclusion _ _ _ x xInComplementClosureInteriorA).\n rewrite <- interior_fixes_open with (S:=interior A) at 1.\n eauto with sets.\n apply interior_open.\nQed.\n\nTheorem incl_frontier2 (X:TopologicalSpace) (A:Ensemble (point_set X)):\n Included (frontier X (closure A)) (frontier X A).\nProof.\n autounfold. autorewrite with sets_helper. autounfold with sets.\n rewrite closure_fixes_closed. intros _ [x xInClosureA xInComplementInteriorClosureA]. constructor.\n + apply xInClosureA.\n + refine (complement_inclusion _ _ _ x xInComplementInteriorClosureA). refine (interior_increasing _ _ _).\n apply closure_inflationary.\n + apply closure_closed.\nQed.\n<\/pre><\/div>\n\n\nL’inclusion de la fronti\u00e8re de l’union dans l’union des fronti\u00e8res est \u00e9galement assez directe (surtout si on s’autorise des eauto) :<\/p>\n\n\n
\nTheorem front_union (X:TopologicalSpace): forall A B, Included (frontier X (Union A B)) (Union (frontier X A) (frontier X B)).\nProof. \n intros. autounfold. autorewrite with sets_helper.\n rewrite closure_union.\n\n unfold Included.\n intros _ [x xInUClAClB xInComplementIntUAB].\n destruct xInUClAClB as [x0 xInClosureA | x0 xInClosureB].\n - left. constructor.\n * apply xInClosureA.\n * refine (complement_inclusion _ _ _ x0 xInComplementIntUAB).\n apply interior_increasing. eauto with sets.\n - right. constructor.\n * apply xInClosureB.\n * refine (complement_inclusion _ _ _ x0 xInComplementIntUAB).\n apply interior_increasing. eauto with sets.\nQed.\n<\/pre><\/div>\n\n\nEn revanche les choses se corsent pour d\u00e9montrer l’inclusion inverse dans le cas de la disjonction des adh\u00e9rences.<\/p>\n","protected":false},"excerpt":{"rendered":"
Alors celui l\u00e0, il est costaud malgr\u00e9 son apparente simplicit\u00e9. Commen\u00e7ons par l\u2019\u00e9nonc\u00e9 : Dans un espace topologique, on d\u00e9finit la fronti\u00e8re d\u2019une partie A comme \u00e9tant . Montrer que et que ferm\u00e9 d\u2019int\u00e9rieur vide. Montrer que et sont toutes deux incluses dans , et donner un exemple o\u00f9 ces inclusions sont strictes. Montrer que , […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[2],"tags":[],"_links":{"self":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/98"}],"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=98"}],"version-history":[{"count":7,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/98\/revisions"}],"predecessor-version":[{"id":105,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/98\/revisions\/105"}],"wp:attachment":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=98"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=98"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=98"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}