From d3e4c784c6a5b3d99144065c6bf12de67e95d41a Mon Sep 17 00:00:00 2001 From: Damien Rouhling Date: Mon, 3 Aug 2020 10:02:49 +0200 Subject: [PATCH 1/2] Generalise closeness properties to uniform spaces --- CHANGELOG_UNRELEASED.md | 5 ++- theories/topology.v | 96 ++++++++++++++++++++++++++--------------- 2 files changed, 66 insertions(+), 35 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 54b2b20fd3..4276f2a6ef 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,7 +18,8 @@ `subset_split_ent`, `entourage_split`, `nbhs_entourage`, `cvg_entourageP`, `cvg_entourage`, `cvg_app_entourageP`, `cvg_mx_entourageP`, `cvg_fct_entourageP`, `entourage_E`, `entourage_ballE`, - `entourage_from_ballE`, `entourage_ball`, `entourage_proper_filter` + `entourage_from_ballE`, `entourage_ball`, `entourage_proper_filter`, + `open_nbhs_entourage`, `entourage_close` + `completePseudoMetricType` structure + `completePseudoMetricType` structure on matrices and function spaces - in `classical_sets.v`: @@ -62,6 +63,8 @@ `R_uniformType`, `R_pseudoMetricType` + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_nbhs'`, `nbhs_pt_comp` + + lemmas `close_trans`, `close_cvgxx`, `cvg_closeP` and `close_cluster` are + valid for a `uniformType` ### Renamed diff --git a/theories/topology.v b/theories/topology.v index 0f6b6ec13b..01b039da3d 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2854,6 +2854,68 @@ Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core. Arguments entourage_split {M} z {x y A}. Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core. +Section uniform_closeness. + +Variable (U : uniformType). + +Lemma open_nbhs_entourage (x : U) (A : set (U * U)) : + entourage A -> open_nbhs x (to_set A x)^°. +Proof. +move=> entA; split; first exact: open_interior. +by apply: nbhs_singleton; apply: nbhs_interior; apply: nbhs_entourage. +Qed. + +Lemma entourage_close (x y : U) : + close x y = forall A, entourage A -> A (x, y). +Proof. +rewrite propeqE; split=> [cxy A entA|cxy]. + have /entourage_split_ent entsA := entA. + have [z [/interior_subset zx /interior_subset /= zy]] := + cxy _ (open_nbhs_entourage _ (entourage_inv entsA)) + _ (open_nbhs_entourage _ entsA). + exact: (entourage_split z). +move=> A /open_nbhs_nbhs/nbhsP[E1 entE1 sE1A]. +move=> B /open_nbhs_nbhs/nbhsP[E2 entE2 sE2B]. +by exists y; split; [apply/sE2B; apply: cxy|apply/sE1A; apply: entourage_refl]. +Qed. + +Lemma close_trans (y x z : U) : close x y -> close y z -> close x z. +Proof. +rewrite !entourage_close => cxy cyz A entA. +exact: entourage_split (cxy _ _) (cyz _ _). +Qed. + +Lemma close_cvgxx (x y : U) : close x y -> x --> y. +Proof. +rewrite entourage_close => cxy P /= /nbhsP[A entA sAP]. +apply/nbhsP; exists (split_ent A) => // z xz; apply: sAP. +apply: (entourage_split x) => //. +by have := cxy _ (entourage_inv (entourage_split_ent entA)). +Qed. + +Lemma cvg_closeP (F : set (set U)) (l : U) : ProperFilter F -> + F --> l <-> ([cvg F in U] /\ close (lim F) l). +Proof. +move=> FF; split=> [Fl|[cvF]Cl]. + by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F). +by apply: cvg_trans (close_cvgxx Cl). +Qed. + +Lemma close_cluster (x y : U) : close x y = cluster (nbhs x) y. +Proof. +rewrite propeqE; split => xy. +- move=> A B xA; rewrite -nbhs_entourageE => -[E entE sEB]. + exists x; split; first exact: nbhs_singleton. + by apply/sEB; move/close_sym: xy; rewrite entourage_close; apply. +- rewrite entourage_close => A entA. + have /entourage_split_ent entsA := entA. + have [z [/= zx zy]] := + xy _ _ (nbhs_entourage _ entsA) (nbhs_entourage _ (entourage_inv entsA)). + exact: (entourage_split z). +Qed. + +End uniform_closeness. + Definition unif_continuous (U V : uniformType) (f : U -> V) := (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage. @@ -3393,26 +3455,6 @@ move=> A /open_nbhs_nbhs/nbhs_ballP[_/posnumP[e1 e1A]]. by exists y; split; [apply/e1A|apply/e2B/ballxx]. Qed. -Lemma close_trans (y x z : M) : close x y -> close y z -> close x z. -Proof. -by rewrite !ball_close => cxy cyz eps; apply: ball_split (cxy _) (cyz _). -Qed. - -Lemma close_cvgxx (x y : M) : close x y -> x --> y. -Proof. -rewrite ball_close => cxy P /= /nbhs_ballP /= [_/posnumP [eps] epsP]. -apply/nbhs_ballP; exists (eps%:num / 2) => // z bxz. -by apply: epsP; apply: ball_splitr (cxy _) bxz. -Qed. - -Lemma cvg_closeP (F : set (set M)) (l : M) : ProperFilter F -> - F --> l <-> ([cvg F in M] /\ close (lim F) l). -Proof. -move=> FF; split=> [Fl|[cvF]Cl]. - by have /cvgP := Fl; split=> //; apply: (@cvg_close _ F). -by apply: cvg_trans (close_cvgxx Cl). -Qed. - End pseudoMetricType_numFieldType. Section ball_hausdorff. @@ -3435,20 +3477,6 @@ by rewrite (subsetI_eq0 _ _ brs_eq0)//; apply: interior_subset. Qed. End ball_hausdorff. -Lemma close_cluster (R : numFieldType) (T : pseudoMetricType R) (x y : T) : - close x y = cluster (nbhs x) y. -Proof. -rewrite propeqE; split => xy. -- move=> A B xA; rewrite -nbhs_ballE => -[_/posnumP[e] yeB]. - exists x; split; first exact: nbhs_singleton. - by apply/yeB/ball_sym; move: e {yeB}; rewrite -ball_close. -- rewrite ball_close => e. - have e20 : 0 < e%:num / 2 by apply: divr_gt0. - set e2 := PosNum e20. - case: (xy _ _ (nbhsx_ballx x e2) (nbhsx_ballx y e2)) => z [xz /ball_sym zy]. - by rewrite (splitr e%:num); exact: (ball_triangle xz). -Qed. - Section entourages. Variable R : numDomainType. Lemma unif_continuousP (U V : pseudoMetricType R) (f : U -> V) : From c07d14abb1735b59f76d01ca5f1337e8b24f59aa Mon Sep 17 00:00:00 2001 From: Damien Rouhling Date: Mon, 3 Aug 2020 14:56:51 +0200 Subject: [PATCH 2/2] Generalise continuous_withinNx --- CHANGELOG_UNRELEASED.md | 2 ++ theories/topology.v | 13 +++++++++++++ 2 files changed, 15 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4276f2a6ef..0c8e77f6ff 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -65,6 +65,8 @@ `continuity_pt_cvg'`, `continuity_pt_nbhs'`, `nbhs_pt_comp` + lemmas `close_trans`, `close_cvgxx`, `cvg_closeP` and `close_cluster` are valid for a `uniformType` + + moved `continuous_withinNx` from `normedType.v` to `topology.v` and + generalised it to `uniformType` ### Renamed diff --git a/theories/topology.v b/theories/topology.v index 01b039da3d..3b21921870 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2854,6 +2854,19 @@ Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core. Arguments entourage_split {M} z {x y A}. Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core. +Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x : + {for x, continuous f} <-> f @ nbhs' x --> f x. +Proof. +split=> - cfx P /= fxP. + rewrite /nbhs' !near_simpl near_withinE. + by rewrite /nbhs'; apply: cvg_within; apply/cfx. + (* :BUG: ssr apply: does not work, + because the type of the filter is not inferred *) +rewrite !nbhs_nearE !near_map !near_nbhs in fxP *; have /= := cfx P fxP. +rewrite !near_simpl near_withinE near_simpl => Pf; near=> y. +by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y]. +Grab Existential Variables. all: end_near. Qed. + Section uniform_closeness. Variable (U : uniformType).