Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce T_0 and T_1 spaces and prove T_1 -> T0. #438

Merged
merged 4 commits into from
Jan 6, 2022
Merged

Introduce T_0 and T_1 spaces and prove T_1 -> T0. #438

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a278031
Introduce T_0 and T_1 spaces and prove T_1 -> T0.
vlj Sep 26, 2021
6464cc1
formatting
affeldt-aist Oct 13, 2021
b77e7f3
fix
CohenCyril Dec 8, 2021
c959eee
renaming
affeldt-aist Dec 29, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,21 @@

### Added

- in `topology.v`:
+ definitions `kolmogorov_space`, `accessible_space`
+ lemmas `accessible_closed_set1`, `accessible_kolmogorov`

### Changed

- in `topology.v`:
+ renamed and generalized `setC_subset_set1C` implication to
equivalence `subsetC1`

### Renamed

- in `topology.v:
+ `hausdorff` -> `hausdorff_space`

### Removed

### Infrastructure
Expand Down
8 changes: 7 additions & 1 deletion theories/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ Require Import boolp.
(* A.`2 == set of points a such that there exists b so *)
(* that A (b, a). *)
(* ~` A == complement of A. *)
(* [set ~ a] == complement of [set a]. *)
(* [set~ a] == complement of [set a]. *)
(* A `\` B == complement of B in A. *)
(* A `\ a == A deprived of a. *)
(* \bigcup_(i in P) F == union of the elements of the family F whose *)
Expand Down Expand Up @@ -492,6 +492,12 @@ Proof. by rewrite subsets_disjoint setCK. Qed.

Lemma setCT : ~` setT = set0 :> set T. Proof. by rewrite -setC0 setCK. Qed.

Lemma subsetC1 x A : (A `<=` [set~ x]) = (x \in ~` A).
Proof.
rewrite !inE; apply/propext; split; first by move/[apply]; apply.
by move=> NAx y; apply: contraPnot => ->.
Qed.

Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.

Lemma setSD C A B : A `<=` B -> A `\` C `<=` B `\` C.
Expand Down
19 changes: 10 additions & 9 deletions theories/normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum finmap.
From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
From mathcomp Require Import seq fintype bigop order ssralg ssrint ssrnum.
From mathcomp Require Import finmap matrix interval zmodp vector fieldext.
From mathcomp Require Import falgebra.
Require Import boolp ereal reals cardinality.
Require Import classical_sets posnum nngnum topology prodnormedzmodule.

Expand Down Expand Up @@ -1626,7 +1627,7 @@ Local Notation ball_norm := (ball_ (@normr R V)).

Local Notation nbhs_norm := (@nbhs_ball _ V).

Lemma norm_hausdorff : hausdorff V.
Lemma norm_hausdorff : hausdorff_space V.
Proof.
rewrite ball_hausdorff => a b ab.
have ab2 : 0 < `|a - b| / 2 by apply divr_gt0 => //; rewrite normr_gt0 subr_eq0.
Expand All @@ -1637,7 +1638,7 @@ move: (ltr_add acr bcr); rewrite -r22 (distrC b c).
move/(le_lt_trans (ler_dist_add c a b)).
by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE.
Qed.
Hint Extern 0 (hausdorff _) => solve[apply: norm_hausdorff] : core.
Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core.

(* TODO: check if the following lemma are indeed useless *)
(* i.e. where the generic lemma is applied, *)
Expand Down Expand Up @@ -1734,7 +1735,7 @@ Proof. by move=> ?; rewrite normmZ normfV normr_id mulVf ?normr_eq0. Qed.

End NormedModule_numFieldType.
Arguments cvg_bounded {_ _ F FF}.
Hint Extern 0 (hausdorff _) => solve[apply: norm_hausdorff] : core.
Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core.

Module Export NbhsNorm.
Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).
Expand All @@ -1743,7 +1744,7 @@ End NbhsNorm.
(* TODO: generalize to R : numFieldType *)
Section hausdorff.

Lemma Rhausdorff (R : realFieldType) : hausdorff R.
Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
Proof.
move=> x y clxy; apply/eqP; rewrite eq_le.
apply/in_segment_addgt0Pr => _ /posnumP[e].
Expand All @@ -1755,7 +1756,7 @@ Qed.

Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType)
(V : pseudoMetricNormedZmodType R) :
hausdorff V.
hausdorff_space V.
Proof.
move=> p q clp_q; apply/subr0_eq/normr0_eq0/Rhausdorff => A B pq_A.
rewrite -(@normr0 _ V) -(subrr p) => pp_B.
Expand Down Expand Up @@ -3740,7 +3741,7 @@ rewrite nbhsE /=; eexists; split; last by move=> y; exact.
by split; [apply open_ereal_lt_ereal | rewrite /= lte_ninfty].
Qed.

Lemma ereal_hausdorff : hausdorff (ereal_topologicalType R).
Lemma ereal_hausdorff : hausdorff_space (ereal_topologicalType R).
Proof.
move=> -[r| |] // [r' | |] //=.
- move=> rr'; congr (_%:E); apply Rhausdorff => /= A B rA r'B.
Expand Down Expand Up @@ -3771,7 +3772,7 @@ Qed.

End ereal_is_hausdorff.

Hint Extern 0 (hausdorff _) => solve[apply: ereal_hausdorff] : core.
Hint Extern 0 (hausdorff_space _) => solve[apply: ereal_hausdorff] : core.

Section limit_composition_ereal.

Expand Down
71 changes: 47 additions & 24 deletions theories/topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -208,11 +208,13 @@ Require Import boolp reals classical_sets posnum.
(* cluster F == set of cluster points of F. *)
(* compact == set of compact sets w.r.t. the filter- *)
(* based definition of compactness. *)
(* hausdorff T <-> T is a Hausdorff space (T_2). *)
(* hausdorff_space T <-> T is a Hausdorff space (T_2). *)
(* cover_compact == set of compact sets w.r.t. the open *)
(* cover-based definition of compactness. *)
(* connected A <-> the only non empty subset of A which *)
(* is both open and closed in A is A. *)
(* kolmogorov_space T <-> T is a Kolmogorov space (T_0). *)
(* accessible_space T <-> T is an accessible space (T_1). *)
(* separated A B == the two sets A and B are separated *)
(* component x == the connected component of point x *)
(* [locally P] := forall a, A a -> G (within A (nbhs x)) *)
Expand Down Expand Up @@ -2676,7 +2678,7 @@ have [|p [Bp Fp]] := Bco F; first exact: filterS FA.
by exists p; split=> //; apply: Acl=> C Cp; apply: Fp.
Qed.

Definition hausdorff := forall p q : T, cluster (nbhs p) q -> p = q.
Definition hausdorff_space := forall p q : T, cluster (nbhs p) q -> p = q.

Typeclasses Opaque within.
Global Instance within_nbhs_proper (A : set T) p :
Expand All @@ -2686,15 +2688,15 @@ move=> clAp; apply: Build_ProperFilter => B.
by move=> /clAp [q [Aq AqsoBq]]; exists q; apply: AqsoBq.
Qed.

Lemma compact_closed (A : set T) : hausdorff -> compact A -> closed A.
Lemma compact_closed (A : set T) : hausdorff_space -> compact A -> closed A.
Proof.
move=> hT Aco p clAp; have pA := !! @withinT _ (nbhs p) A _.
have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //.
by apply: cvg_cluster clsAp_q; apply: cvg_within.
Qed.

End Compact.
Arguments hausdorff : clear implicits.
Arguments hausdorff_space : clear implicits.

Lemma continuous_compact (T U : topologicalType) (f : T -> U) A :
{in A, continuous f} -> compact A -> compact (f @` A).
Expand Down Expand Up @@ -3007,10 +3009,31 @@ End Covers.

Section separated_topologicalType.
Variable (T : topologicalType).
Implicit Types x y : T.

Local Open Scope classical_set_scope.

Definition close (x y : T) : Prop := forall M, open_nbhs y M -> closure M x.
Definition kolmogorov_space := forall x y, x != y ->
exists A : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).

Definition accessible_space := forall x y, x != y ->
exists A : set T, open A /\ x \in A /\ y \in ~` A.

Lemma accessible_closed_set1 : accessible_space -> forall x, closed [set x].
Proof.
move=> T1 x; rewrite -[X in closed X]setCK; apply: closedC.
rewrite openE => y /eqP /T1 [U [oU [yU xU]]].
rewrite /interior nbhsE /=; exists U; split; last by rewrite subsetC1.
by split=> //; rewrite inE in yU.
Qed.

Definition accessible_kolmogorov : accessible_space -> kolmogorov_space.
Proof.
move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //.
by rewrite nbhsE inE; exists A; do !split=> //; rewrite inE in xA.
Qed.

Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.

Lemma closeEnbhs x : close x = cluster (nbhs x).
Proof.
Expand All @@ -3026,16 +3049,15 @@ Proof.
by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
Qed.

Lemma close_sym (x y : T) : close x y -> close y x.
Lemma close_sym x y : close x y -> close y x.
Proof. by rewrite !closeEnbhs /cluster/= meetsC. Qed.

Lemma cvg_close {F} {FF : ProperFilter F} (x y : T) :
F --> x -> F --> y -> close x y.
Lemma cvg_close {F} {FF : ProperFilter F} x y : F --> x -> F --> y -> close x y.
Proof.
by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx.
Qed.

Lemma close_refl (x : T) : close x x.
Lemma close_refl x : close x x.
Proof. exact: (@cvg_close (nbhs x)). Qed.
Hint Resolve close_refl : core.

Expand All @@ -3049,7 +3071,7 @@ have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
rewrite dvgP // dvgP //; exact/close_refl.
Qed.

Lemma cvgx_close (x y : T) : x --> y -> close x y.
Lemma cvgx_close x y : x --> y -> close x y.
Proof. exact: cvg_close. Qed.

Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
Expand All @@ -3063,14 +3085,14 @@ by rewrite fmapiE; apply: filterS => x [y []]; exists y.
Grab Existential Variables. all: end_near. Qed.
Definition cvg_toi_locally_close := @cvgi_close.

Lemma open_hausdorff : hausdorff T =
(forall x y : T, x != y ->
Lemma open_hausdorff : hausdorff_space T =
forall x y, x != y ->
exists2 AB, (x \in AB.1 /\ y \in AB.2) &
[/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0]).
[/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
Proof.
rewrite propeqE; split => [T_filterT2|T_openT2] x y.
have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP) => cl /cl.
rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
move=> /[apply]; rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
rewrite forallbE => /existsp_asboolPn/=[A]/negP/existsp_asboolPn/=[B].
rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].
Expand All @@ -3084,24 +3106,24 @@ move=> /(_ A B (open_nbhs_nbhs _) (open_nbhs_nbhs _)).
by rewrite -set0P => /(_ _ _)/negP; apply.
Qed.

Hypothesis sep : hausdorff T.
Hypothesis sep : hausdorff_space T.

Lemma closeE (x y : T) : close x y = (x = y).
Lemma closeE x y : close x y = (x = y).
Proof.
rewrite propeqE; split; last by move=> ->; exact: close_refl.
by rewrite closeEnbhs; exact: sep.
Qed.

Lemma close_eq (y x : T) : close x y -> x = y.
Lemma close_eq x y : close x y -> x = y.
Proof. by rewrite closeE. Qed.

Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.

Lemma cvg_eq (x y : T) : x --> y -> x = y.
Lemma cvg_eq x y : x --> y -> x = y.
Proof. by rewrite -closeE //; apply: cvg_close. Qed.

Lemma lim_id (x : T) : lim x = x.
Lemma lim_id x : lim x = x.
Proof. by apply/esym/cvg_eq/cvg_ex; exists x. Qed.

Lemma cvg_lim {F} {FF : ProperFilter F} (l : T) : F --> l -> lim F = l.
Expand Down Expand Up @@ -4077,9 +4099,10 @@ End pseudoMetricType_numFieldType.
Section ball_hausdorff.
Variables (R : numDomainType) (T : pseudoMetricType R).

Lemma ball_hausdorff : hausdorff T =
Lemma ball_hausdorff : hausdorff_space T =
forall (a b : T), a != b ->
exists r : {posnum R} * {posnum R}, ball a r.1%:num `&` ball b r.2%:num == set0.
exists r : {posnum R} * {posnum R},
ball a r.1%:num `&` ball b r.2%:num == set0.
Proof.
rewrite propeqE open_hausdorff; split => T2T a b /T2T[[/=]].
move=> A B; rewrite 2!inE => [[aA bB] [oA oB /eqP ABeq0]].
Expand Down Expand Up @@ -5147,7 +5170,7 @@ by rewrite eqfg ?inE //; exact: entourage_refl.
Qed.

Lemma hausdorrf_close_eq_in (A : set U) (f g : {uniform` A -> V}) :
hausdorff V -> close f g = {in A, f =1 g}.
hausdorff_space V -> close f g = {in A, f =1 g}.
Proof.
move=> hV.
rewrite propeqE; split; last exact: eq_in_close.
Expand Down Expand Up @@ -5497,7 +5520,7 @@ Lemma open_subspaceW (U : set T) :
Proof. by move=> oU; apply/open_subspaceP; exists U. Qed.

Lemma subspace_hausdorff :
hausdorff T -> hausdorff [topologicalType of subspace A].
hausdorff_space T -> hausdorff_space [topologicalType of subspace A].
Proof.
rewrite ?open_hausdorff => + x y xNy => /(_ x y xNy).
move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ].
Expand Down