On continue dans la s\u00e9rie d’exercice autour de la topologie, cette fois-ci en rentrant un peu plus dans le sujet en manipulant les concepts d’int\u00e9rieur et d’adh\u00e9rence.
Le module coq topology fournit une d\u00e9finition de ces concepts, ainsi que plusieurs propri\u00e9t\u00e9s usuelles (inclusions diverses, relation avec les compl\u00e9ments, caract\u00e9risation par la rencontre non vide etc) ; j’ai senti moins d’absences \u00e9tranges que dans le cas des unions de familles comme dans les 2 exercices pr\u00e9c\u00e9dents.
Le sujet, toujours tir\u00e9 de la m\u00eame feuille d’exercice :
<\/p>\n\n\n\n
Si \\(A\\) est une partie de l\u2019espace topologique \\(X\\), on pose \\(\\alpha(A) = \\mathring{\\overline{A}}\\) et \\(\\beta(A) = \\overline{\\mathring{A}}\\).
Montrer que \\(\\alpha\\) et \\(\\beta]\\) sont des applications croissantes pour l\u2019inclusion de \\(\\mathcal{P}(X)\\) dans \\(\\mathcal{P}(X)\\).
Montrer que si \\(A\\) est ouvert, \\(A\\subset\\alpha(A)\\) et si \\(A\\) est ferm\u00e9, \\(\\beta(A)\\subset A\\). En d\u00e9duire que
\\(\\alpha^2 = \\alpha\\) et \\(\\beta^2 = \\beta\\).<\/p><\/blockquote>\n\n\n\nOn va traduire les d\u00e9finitions en Coq :<\/p>\n\n\n
\nFrom Topology Require Import InteriorsClosures. \n\nDefinition alpha (X:TopologicalSpace) (A:Ensemble (point_set X)) :=\ninterior (closure A). \n\nDefinition beta (X:TopologicalSpace) (A:Ensemble (point_set X)) := \nclosure (interior A).\n<\/pre><\/div>\n\n\nLa croissance est relativement facile \u00e0 prouver \u00e0 partir de la croissance des int\u00e9rieurs fourni par le module topology et adh\u00e9rences et en tripatouillant les d\u00e9finitions :<\/p>\n\n\n
\nTheorem croiss (X:TopologicalSpace) :\n forall A B, Included A B -> Included (alpha X A) (alpha X B).\nProof.\n unfold alpha. unfold Included. intros A B H x.\n apply interior_increasing. apply closure_increasing.\n unfold Included. apply H.\nQed.\n<\/pre><\/div>\n\n\nProuver les inclusions est \u00e9galement relativement simple :<\/p>\n\n\n
\nTheorem open_alpha (X:TopologicalSpace) :\n forall A: Ensemble (point_set X), open A -> Included A (alpha X A). Proof.\n unfold alpha. intros. Search (interior). apply interior_maximal.\n apply H. apply closure_inflationary.\nQed.\n\nTheorem closure_beta (X:TopologicalSpace) :\n forall A: Ensemble (point_set X), closed A -> Included (beta X A) A.\nProof.\n unfold beta. intros. Search (closure). apply closure_minimal.\n apply H. Search (interior). apply interior_deflationary.\nQed.\n<\/pre><\/div>\n\n\nLa derni\u00e8re propri\u00e9t\u00e9 est un peu plus d\u00e9licate \u00e0 prouver. D\u00e9plier les d\u00e9finitions n’est pas suffisant… Il faut en effet reconnaitre \\(\\alpha\\) dans l’expression de \\(\\beta^2\\) et r\u00e9ciproqement pour appliquer la propri\u00e9t\u00e9 pr\u00e9c\u00e9dente.<\/p>\n\n\n
\nRequire Import Coq.Logic.FunctionalExtensionality. \n\nTheorem alpha_square (X:TopologicalSpace):\n alpha X = fun A => alpha X (alpha X A).\nProof.\n\u00a0\u00a0 apply functional_extensionality. intros.\n apply Extensionality_Ensembles. unfold Same_set. split.\n\u00a0\u00a0 - apply open_alpha. Search (interior). apply interior_open.\n\u00a0\u00a0 - unfold alpha in *. pose(tmp:=closure_beta X (closure x)).\n unfold beta in tmp. Search (interior).\n apply interior_increasing. apply tmp. apply closure_closed.\n Qed.\n<\/pre><\/div>","protected":false},"excerpt":{"rendered":"On continue dans la s\u00e9rie d’exercice autour de la topologie, cette fois-ci en rentrant un peu plus dans le sujet en manipulant les concepts d’int\u00e9rieur et d’adh\u00e9rence. Le module coq topology fournit une d\u00e9finition de ces concepts, ainsi que plusieurs propri\u00e9t\u00e9s usuelles (inclusions diverses, relation avec les compl\u00e9ments, caract\u00e9risation par la rencontre non vide etc) […]<\/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\/71"}],"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=71"}],"version-history":[{"count":7,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/71\/revisions"}],"predecessor-version":[{"id":89,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=\/wp\/v2\/posts\/71\/revisions\/89"}],"wp:attachment":[{"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=71"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=71"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/pinkieduck.net\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=71"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}