On continue dans la série d’exercice autour de la topologie, cette fois-ci en rentrant un peu plus dans le sujet en manipulant les concepts d’intérieur et d’adhérence.
Le module coq topology fournit une définition de ces concepts, ainsi que plusieurs propriétés usuelles (inclusions diverses, relation avec les compléments, caractérisation par la rencontre non vide etc) ; j’ai senti moins d’absences étranges que dans le cas des unions de familles comme dans les 2 exercices précédents.

Le sujet, toujours tiré de la même feuille d’exercice :

Si \(A\) est une partie de l’espace 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’inclusion de \(\mathcal{P}(X)\) dans \(\mathcal{P}(X)\).
Montrer que si \(A\) est ouvert, \(A\subset\alpha(A)\) et si \(A\) est fermé, \(\beta(A)\subset A\). En déduire que
\(\alpha^2 = \alpha\) et \(\beta^2 = \beta\).

On va traduire les définitions en Coq :

From Topology Require Import InteriorsClosures. 

Definition alpha (X:TopologicalSpace) (A:Ensemble (point_set X)) :=
interior (closure A). 

Definition beta (X:TopologicalSpace) (A:Ensemble (point_set X)) := 
closure (interior A).

La croissance est relativement facile à prouver à partir de la croissance des intérieurs fourni par le module topology et adhérences et en tripatouillant les définitions :

Theorem croiss (X:TopologicalSpace) :
    forall A B, Included A B -> Included (alpha X A) (alpha X B).
Proof.
   unfold alpha. unfold Included. intros A B H x.
   apply interior_increasing. apply closure_increasing.
   unfold Included. apply H.
Qed.

Prouver les inclusions est également relativement simple :

Theorem open_alpha (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), open A -> Included A (alpha X A). Proof.
    unfold alpha. intros. Search (interior). apply interior_maximal.
    apply H. apply closure_inflationary.
Qed.

Theorem closure_beta (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), closed A -> Included (beta X A) A.
Proof.
   unfold beta. intros. Search (closure). apply closure_minimal.
   apply H. Search (interior). apply interior_deflationary.
Qed.

La dernière propriété est un peu plus délicate à prouver. Déplier les définitions n’est pas suffisant… Il faut en effet reconnaitre \(\alpha\) dans l’expression de \(\beta^2\) et réciproqement pour appliquer la propriété précédente.

Require Import Coq.Logic.FunctionalExtensionality. 

Theorem alpha_square (X:TopologicalSpace):
    alpha X = fun A => alpha X (alpha X A).
Proof.
   apply functional_extensionality. intros.
   apply Extensionality_Ensembles. unfold Same_set. split.
   - apply open_alpha. Search (interior). apply interior_open.
   - unfold alpha in *. pose(tmp:=closure_beta X (closure x)).
       unfold beta in tmp. Search (interior).
       apply interior_increasing. apply tmp. apply closure_closed.
 Qed.