On continue dans la série des espaces topologiques avec un exercice sur les axiomes de séparation :
Soit \((X, T )\) un espace topologique.
Montrer que les conditions suivantes sont équivalentes :
(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é.\)
(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é de points.
Apparté sur la séparation
Cet exercice m’a donné l’occasion de découvrir le concept de séparation en topologie que je ne connaissais que très vaguement. L’idée derrière la séparation est de caractériser le niveau d’ « indépendance » des voisinages de deux points distincts. Plus exactement, on distingue 3 niveaux de séparations notés T0, T1 et T2:
- T0 signifie que si on prend deux points distincts, on a au moins un voisinage de l’un qui ne contient pas l’autre,
- T1 signifie que si on prend deux points distincts, chacun a au moins un voisinage ne contenant pas l’autre,
- 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.
La plupart des espaces usuels (les réels, complexes, espaces vectoriels…) sont T2. Parmi les espaces qui ne sont pas séparés il y a les topologies grossières (ie l’ensemble entier et l’ensemble vide). J’avoue que je ne connais pas la motivation derrière les niveaux T0 et T1 et je n’ai pas d’exemples d’espace vérifiant ces niveaux mais pas les suivants.
Le trio d’équivalence est semble-t-il une propriété fondamentale des axiomes de séparation puisqu’il est directement présenté comme propriété dans mon livre de topologie, qui le démontre de bas en haut. J’ai essayé d’effectuer la démonstration en Coq de haut en bas mais je me suis retrouvé bloquer en cherchant à passer de (ii) à (iii) ; ayant ensuite décidé qu’il était peut-être plus sage de suivre une voie connue, j’ai finalement opté pour la démonstration de bas en haut. Il s’avère que le passage de (iii) à (ii) est aussi compliqué et que dans les autres cas les preuves sont plus ou moins des « miroirs » de celles que j’avais faite dans ma première tentative, j’imagine aisément qu’il est malgré tout possible d’effectuer la preuve dans n’importe quel sens.
Préalable
Une propriété particulièrement utile pour cette exercice est la caractérisation de l’adhérence d’un ensemble, appelé closure_impl_meets_every_open_neighborhood dans coq-topology : un point est dans l’adhérence 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.
Du point de vue plus pratique, on continue à utiliser quelques astuces qui simplifient la vie sur le long terme : on définit une tactic ensemble_proof_intro pour automatiquement nous fournir les 2 inclusions de l’égalité de l’ensemble à prouver, on se sert d’inversion plutôt que de destruct, et on nomme autant que possible les hypothèses/variables pour faciliter la lecture.
A noter qu’à un moment j’ai eu besoin de définir un axiome sur la décidabilité sur l’égalité de 2 éléments d’un ensemble. Par défaut si deux éléments d’un ensemble ne sont pas égaux, Coq ne déduit pas automatiquement qu’ils sont différents ; en effet la logique constructive sur laquelle est basée Coq se passe de l’axiome du tiers exclu qui stipule qu’une propriété (comme ici l’égalité) est vraie ou sa négation est vraie. Il faut donc manuellement indiqué que dans notre cas, c’est vrai.
Trio d’équivalence
On commence par les imports de circonstances et l’écriture des propriétés :
From Topology Require Import TopologicalSpaces.
From Topology Require Import InteriorsClosures.
From Topology Require Import Neighborhoods.
Require Import Decidable.
Definition P1 (X:TopologicalSpace) :=
forall x y:point_set X, not (x = y) -> exists N, neighborhood N x /\ not (In N y).
Definition P2 (X:TopologicalSpace) :=
forall x:point_set X, closed (Singleton x).
Definition P3 (X:TopologicalSpace) :=
forall x:point_set X, FamilyIntersection [V:Ensemble (point_set X) | neighborhood V x] = Singleton x.
Ltac ensemble_proof_intro:=apply Extensionality_Ensembles; unfold Same_set; split.
On aura également besoin de montrer que si un singleton est contenu dans un autre, alors leur élément est égal :
Theorem Singleton_Inclusion (T:Type): forall x y:T, Included (Singleton x) (Singleton y) -> x = y.
Proof.
intros.
unfold Included in H. symmetry. apply Singleton_inv. apply H. eauto with sets.
Qed.
On commence ensuite par l’implication la plus compliqué, P3 vers P2 :
Theorem P3_implies_P2 {X:TopologicalSpace}:
P3 X -> P2 X.
Proof.
unfold P3. unfold P2.
intros P3 x0.
La stratégie pour montrer que le singleton x est fermé, est de montrer qu’il est égal à son adhérence. Cette stratégie part de l’intuition que l’écriture de l’ensemble des voisinages est proche d’une intersection en ensemble de fermé contenant un ensemble.
assert (Included (closure (Singleton x0)) (Singleton x0)).
unfold Included.
intros x xInClosure.
On va se servir de la propriété sur la caractérisation des adhérences. Quand on regarde les hypothèses de cette propriété, on voit qu’il va falloir trouver un ouvert, qui contient x, et on en déduira que x0 est dans V (car l’intersection du singleton x0 et V est non vide).
pose (tmp2:=closure_impl_meets_every_open_neighborhood _ (Singleton x0) x xInClosure).
assert (forall V, open_neighborhood V x -> Inhabited (Intersection (Singleton x0) V)).
intros V VNeighbor. inversion VNeighbor. unfold open_neighborhood in VNeighbor.
apply tmp2.
assumption. assumption.
assert(forall V, open_neighborhood V x -> In V x0).
intros. pose (tmp3:=H V H0). inversion tmp3. inversion H1. inversion H2. subst. assumption.
Pour rappel, on cherche à montrer ici que x est dans le singleton x0, ie que x = x0. Pour l’instant on n’a pas encore utilisé l’hypothèse P3. Pour se simplifier la vie on peut remarquer qu’on peut se servir des voisinages ouverts plutôt que des voisinages quelconques :
assert( forall x : point_set X, FamilyIntersection [V : Ensemble (point_set X) | neighborhood V x] =
FamilyIntersection [V : Ensemble (point_set X) | open_neighborhood V x]).
{
intros x1. ensemble_proof_intro.
- intros S SinInters. inversion SinInters.
constructor. intros. apply H1. inversion H3. constructor. apply open_neighborhood_is_neighborhood. apply H4.
- intros y yinIntersOpen. inversion yinIntersOpen.
constructor. intros S SInInters. inversion SInInters as [[S' [OpenS' S'InS]]].
refine (S'InS _ _). apply H1. split. assumption.
}
Muni de ce résultat on peut prouver l’égalité:
assert(Included (Singleton x0) (Singleton x)).
unfold Included. intros y yisx0. inversion yisx0.
rewrite <- (P3 x).
rewrite (H1 x).
constructor.
intros. inversion H3. subst. eauto.
et donc l’inclusion inverse :
apply Singleton_intro.
refine (Singleton_Inclusion _ _ _ _). assumption.
La suite est relativement directe:
assert (closure (Singleton x0) = Singleton x0).
ensemble_proof_intro.
apply H. apply closure_inflationary.
rewrite <- H0. apply closure_closed.
Qed.
L’inclusion P2 vers P1 est plus simple:
Theorem P2_implies_P1 {X:TopologicalSpace}:
P2 X -> P1 X.
Proof.
unfold P1, P2.
intros P2 x y xNeqy.
unfold closed in P2.
exists (Complement (Singleton y)). split.
unfold neighborhood. exists (Complement (Singleton y)). split. unfold open_neighborhood. split. apply (P2 y).
unfold Complement. unfold not. unfold In. intros. destruct xNeqy. inversion H. trivial.
eauto with sets.
eauto with sets.
Qed.
Celle de P1 vers P3 n’est pas beaucoup plus compliqué, mais nécessite quand même la décidabilité dont on a préalablement parlé, pour faire une disjonction de cas :
Theorem P1_implies_P3 {X:TopologicalSpace}:
P1 X -> P3 X.
Proof.
unfold P1. unfold P3.
intros P1 x0.
ensemble_proof_intro.
- unfold Included. intros x xInIntersNeigh.
destruct (decT X x0 x).
+ eauto with sets.
+ inversion xInIntersNeigh. destruct (P1 x0 x H). inversion H2. pose (tmp:= H0 x2). autounfold with sets in tmp.
assert([V : Ensemble (point_set X) | neighborhood V x0] x2).
constructor. assumption.
apply tmp in H5. destruct (H4 H5).
- unfold Included. intros x xIsx0.
inversion xIsx0.
constructor. intros. inversion H0. inversion H1. inversion H2. unfold Included in H4. apply H4. inversion H3. assumption.
Qed.
Seconde propriété
Alors là c’est vraiment costaud à démontrer, la faute à la démonstration de l’infinité. Coq dispose de quelques résultats 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éder par l’absurde.
En particulier une propriété des ouverts qui est vraie dans le cas des ensembles finies mais qui ne l’est plus dans les ensembles infinis est la stabilité par intersection. On va donc prouver cette propriété, par récursion sur la taille de l’ensemble :
Theorem intersection_finite (X:TopologicalSpace):
forall F:Family (point_set X), Finite _ F /\ (forall S, In F S -> open S) -> open (FamilyIntersection F).
Proof.
intros F [F_Finite F_Set_Of_Opens].
apply finite_cardinal in F_Finite.
destruct F_Finite as [n cardFn].
generalize dependent F.
induction n ; intros F cardFn F_Set_Of_Opens.
- inversion cardFn. Search FamilyIntersection. rewrite empty_family_intersection.
Print TopologicalSpace. apply open_full.
- inversion cardFn. pose (tmp:= IHn A H0).
assert(FamilyIntersection (Add A x) = Intersection (FamilyIntersection A) x).
ensemble_proof_intro; unfold Included; intros x0.
+ intros x0InIntersAx.
inversion x0InIntersAx.
constructor.
* constructor. eauto with sets.
* eauto with sets.
+ intros x0InInters. inversion x0InInters. inversion H3. constructor. unfold Add.
intros. inversion H8.
* eauto with sets.
* inversion H9. subst. eauto with sets.
+ rewrite H3. apply open_intersection2.
* apply tmp. intros. apply F_Set_Of_Opens. Search Add.
unfold Add in H1. rewrite <- H1. eauto with sets.
* apply F_Set_Of_Opens. rewrite <- H1. unfold Add. eauto with sets.
Qed.
Un autre résultat qui m’a été utile est que l’égalité est conservée par passage au complément :
Theorem Complement_inv (X:Type) : forall (S1 S2: Ensemble X), Complement S1 = Complement S2 -> S1 = S2.
Proof.
intros. ensemble_proof_intro; rewrite <- Complement_Complement with (A:=S1); rewrite <- Complement_Complement with (A:=S2); apply complement_inclusion; rewrite H; eauto with sets.
Qed.
On peut ensuite passer à la démonstration en elle-même :
Theorem 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)).
Proof.
intros P2 A x0 x0inclAminA.
unfold Top.P2 in P2.
destruct x0inclAminA as [x0InClA x0NotInA].
intros N [O [[OpenO x0inO] OInN]].
pose (tmp:=closure_impl_meets_every_open_neighborhood _ A x0 x0InClA).
unfold not. intros NInterAFinite.
remember (fun E => exists x, In (Intersection N A) x /\ E = Complement (Singleton x)) as SetOfElems.
(**pose (tmp3:=intersection_finite _ SetOfElems).**)
assert(Finite _ SetOfElems).
generalize dependent SetOfElems.
induction NInterAFinite; intros.
- assert (SetOfElems = Empty_set). rewrite HeqSetOfElems. ensemble_proof_intro.
+ unfold Included. intros. unfold In in H. destruct H. destruct H. destruct H.
+ eauto with sets.
+ rewrite H. eauto with sets.
- assert (SetOfElems = Add (fun E : Ensemble (point_set X) => exists x0 : point_set X, In A0 x0 /\ E = Complement (Singleton x0)) (Complement (Singleton x))).
ensemble_proof_intro ; unfold Included; rewrite HeqSetOfElems.
+ intros. inversion H0. inversion H1. unfold In. inversion H2 as [x2InA0|].
* left. exists x2. split. assumption. assumption.
* right. inversion H4. subst. eauto with sets.
+ intros. unfold In. inversion H0.
* inversion H1. inversion H3. exists x3. split. left. assumption. assumption.
* exists x. inversion H1. split. right. eauto with sets. trivial.
+ rewrite H0. constructor.
* remember (fun E : Ensemble (point_set X) => exists x1 : point_set X, In A0 x1 /\ E = Complement (Singleton x1)) as P0.
apply IHNInterAFinite. trivial.
* unfold In. unfold not. intros. inversion H1. inversion H2.
apply Complement_inv in H4.
apply Singleton_equal in H4. subst. destruct (H H3).
- remember (FamilyIntersection SetOfElems) as ContraGen.
assert (open ContraGen).
rewrite HeqContraGen.
apply intersection_finite. split.
+ assumption.
+ intros S SInSetOfElems. rewrite HeqSetOfElems in SInSetOfElems. unfold In in SInSetOfElems. inversion SInSetOfElems.
inversion H0. rewrite H2. refine (P2 _).
+ pose (contra:= tmp (Intersection ContraGen O) (open_intersection2 ContraGen O H0 OpenO)).
assert (In (Intersection ContraGen O) x0).
rewrite HeqContraGen.
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.
assumption.
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.
assert(exists x0 : point_set X, Intersection N A x0 /\ Complement (Singleton x) = Complement (Singleton x0)). exists x. split. constructor.
eauto with sets. eauto with sets. trivial. apply contra2 in H11. destruct H11. constructor.
Qed.