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

Products of Hausdorff spaces. #474

Merged
merged 3 commits into from
Jan 21, 2022
Merged

Products of Hausdorff spaces. #474

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
958cc30
linting pass
zstone1 Nov 12, 2021
e3ffa87
renaming and making apply local
zstone1 Jan 20, 2022
2a20c4c
restoring docs
zstone1 Jan 20, 2022
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
43 changes: 43 additions & 0 deletions theories/topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,6 +209,9 @@ Require Import boolp reals classical_sets posnum.
(* compact == set of compact sets w.r.t. the filter- *)
(* based definition of compactness. *)
(* hausdorff_space T <-> T is a Hausdorff space (T_2). *)
(* prod_topo_apply x f == application of f to x, f being in a *)
(* product topology of a family K *)
(* (K : X -> topologicalType) *)
(* 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 *)
Expand Down Expand Up @@ -2873,6 +2876,46 @@ Qed.

End Tychonoff.

Section Product_Hausdorff.
Context {X : choiceType} {K : X -> topologicalType}.

(* This a helper function to prove products preserve hausdorff. In particular *)
(* we use its continuity turn clustering in `product_topologicalType K` to *)
(* clustering in K x for each X. *)
Definition prod_topo_apply x (f : product_topologicalType K) := f x.

Lemma prod_topo_applyE x f : prod_topo_apply x f = f x.
Proof. by []. Qed.

Lemma prod_topo_apply_continuous x : continuous (prod_topo_apply x).
Proof.
move=> f; have /cvg_sup/(_ x)/cvg_image : f --> f by apply: cvg_id.
move=> h; apply: (cvg_trans _ (h _)) => {h}; last first.
pose xval x (y : K x) i : K i :=
match eqVneq x i return K i with
| EqNotNeq r => @eq_rect X x K y i r
| NeqNotEq _ => point
end.
rewrite eqEsubset; split => y //= _; exists (xval x y) => //; rewrite /xval.
by case (eqVneq x x) => [e|/eqP//]; rewrite eq_axiomK.
by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image.
Qed.

Lemma hausdorff_product :
(forall x, hausdorff_space (K x)) -> hausdorff_space (@product_topologicalType X K).
Proof.
move=> hsdfK p q /= clstr; apply: functional_extensionality_dep => x.
apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]].
exists (prod_topo_apply x @ G); [exact: fmap_proper_filter|split].
rewrite -(prod_topo_applyE x).
apply: cvg_trans; last exact: (@prod_topo_apply_continuous x q).
by apply: cvg_app; exact: GtoQ.
move/(cvg_app (prod_topo_apply x)): psubG => /cvg_trans; apply.
exact: prod_topo_apply_continuous.
Qed.

End Product_Hausdorff.

Definition finI (I : choiceType) T (D : set I) (f : I -> set T) :=
forall D' : {fset I}, {subset D' <= D} ->
\bigcap_(i in [set i | i \in D']) f i !=set0.
Expand Down