From 779afdfe680004231dcc1857abcc72946bb27926 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 13 Apr 2023 17:32:49 -0400 Subject: [PATCH] Proof of Urysohn's lemma. PR #900 Co-Authored-By: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 24 +- classical/boolp.v | 14 + classical/classical_sets.v | 8 +- classical/mathcomp_extra.v | 24 ++ theories/constructive_ereal.v | 3 + theories/normedtype.v | 594 ++++++++++++++++++++++++++++++---- theories/topology.v | 126 +++++--- 7 files changed, 677 insertions(+), 116 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ffc9fe2d2..b43828ab4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -36,6 +36,7 @@ - in `mathcomp_extra.v`: + definition `min_fun`, notation `\min` + + new lemmas `maxr_absE`, `minr_absE` - in `classical_sets.v`: + lemmas `set_predC`, `preimage_true`, `preimage_false` - in `lebesgue_measure.v`: @@ -63,22 +64,27 @@ - in `classical_sets.v`: + lemma `Zorn_bigcup` + + lemmas `imsub1` and `imsub1P` + - in file `boolp.v`, + lemmas `notP`, `notE` + new lemma `implyE`. + + new lemmas `contra_leP` and `contra_ltP` + - in file `reals.v`: + lemmas `sup_sumE`, `inf_sumE` - in file `topology.v`: + lemma `ball_symE` - in file `normedtype.v`, + new definition `edist`. - + new lemmas `edist_ge0`, `edist_lt_ball`, + + new lemmas `edist_ge0`, `edist_neqNy`, `edist_lt_ball`, `edist_fin`, `edist_pinftyP`, `edist_finP`, `edist_fin_open`, `edist_fin_closed`, `edist_pinfty_open`, `edist_sym`, `edist_triangle`, `edist_continuous`, `edist_closeP`, and `edist_refl`. - in `constructive_ereal.v`: + lemmas `lte_pmulr`, `lte_pmull`, `lte_nmulr`, `lte_nmull` + lemmas `lte0n`, `lee0n`, `lte1n`, `lee1n` + + lemmas `fine0` and `fine1` - in `sequences.v`: + lemma `eseries_cond` + lemmas `eseries_mkcondl`, `eseries_mkcondr` @@ -100,6 +106,21 @@ + lemmas `Posz_snum_subproof` and `Negz_snum_subproof` + canonical instances `Posz_snum` and `Negz_snum` +- in file `normedtype.v`, + + new definitions `edist_inf`, `uniform_separator`, and `Urysohn`. + + new lemmas `continuous_min`, `continuous_max`, `edist_closel`, + `edist_inf_ge0`, `edist_inf_neqNy`, `edist_inf_triangle`, + `edist_inf_continuous`, `edist_inf0`, `Urysohn_continuous`, + `Urysohn_range`, `Urysohn_sub0`, `Urysohn_sub1`, `Urysohn_eq0`, + `Urysohn_eq1`, `uniform_separatorW`, `normal_uniform_separator`, + `uniform_separatorP`, `normal_urysohnP`, and + `subset_closure_half`. + +- in file `topology.v`, + + new definition `normal_space`. + + new lemmas `filter_inv`, and `countable_uniform_bounded`. + + ### Changed - moved from `lebesgue_measure.v` to `real_interval.v`: @@ -110,6 +131,7 @@ - in `exp.v`: + lemmas `power_posD` (now `powRD`), `power_posB` (now `powRB`) +- moved from `normedtype.v` to `topology.v`: `Rhausdorff`. - in `sequences.v`: + lemma `nneseriesrM` generalized and renamed to `nneseriesZl` diff --git a/classical/boolp.v b/classical/boolp.v index ba8fab556..1bb538d61 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -497,6 +497,20 @@ Proof. by move=> Pxy; apply: contraNP => /Pxy/eqP. Qed. Lemma contra_eqP (T : eqType) (x y : T) (Q : Prop) : (~ Q -> x != y) -> x = y -> Q. Proof. by move=> Qxy /eqP; apply: contraTP. Qed. +Lemma contra_leP {disp1 : unit} {T1 : porderType disp1} [P : Prop] [x y : T1] : + (~ P -> (x < y)%O) -> (y <= x)%O -> P. +Proof. +move=> Pxy yx; apply/asboolP. +by apply: Order.POrderTheory.contra_leT yx => /asboolPn. +Qed. + +Lemma contra_ltP {disp1 : unit} {T1 : porderType disp1} [P : Prop] [x y : T1] : + (~ P -> (x <= y)%O) -> (y < x)%O -> P. +Proof. +move=> Pxy yx; apply/asboolP. +by apply: Order.POrderTheory.contra_ltT yx => /asboolPn. +Qed. + Lemma wlog_neg P : (~ P -> P) -> P. Proof. by move=> ?; case: (pselect P). Qed. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 9b01e6999..5be0229fd 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1244,10 +1244,16 @@ Proof. by split=> fAY x; have := fAY x; rewrite !inE. Qed. Lemma image_subP {A Y f} : f @` A `<=` Y <-> {homo f : x / A x >-> Y x}. Proof. by split=> fAY x => [Ax|[y + <-]]; apply: fAY=> //; exists x. Qed. -Lemma image_sub {f : aT -> rT} {A : set aT} {B : set rT} : +Lemma image_sub {f : aT -> rT} {A : set aT} {B : set rT} : (f @` A `<=` B) = (A `<=` f @^-1` B). Proof. by apply/propext; rewrite image_subP; split=> AB a /AB. Qed. +Lemma imsub1 x A f : f @` A `<=` [set x] -> forall a, A a -> f a = x. +Proof. by move=> + a Aa; apply; exists a. Qed. + +Lemma imsub1P x A f : f @` A `<=` [set x] <-> forall a, A a -> f a = x. +Proof. by split=> [/(@imsub1 _)//|+ _ [a Aa <-]]; apply. Qed. + Lemma image_setU f A B : f @` (A `|` B) = f @` A `|` f @` B. Proof. rewrite eqEsubset; split => b. diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 8e3fd7b7d..98a95abc9 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1392,3 +1392,27 @@ exists f; split => //. intro n; induction n; simpl; apply: proj2_sig. Qed. End dependent_choice_Type. + +Section max_min. +Variable R : realFieldType. +Import Num.Theory. + +Let nz2 : 2 != 0 :> R. Proof. by rewrite pnatr_eq0. Qed. + +Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2. +Proof. +apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//. +case: lerP => _; (* TODO: ring *) rewrite [2]mulr2n mulrDr mulr1. + by rewrite addrACA subrr addr0. +by rewrite addrCA addrAC subrr add0r. +Qed. + +Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2. +Proof. +apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *) +by rewrite -mulrDl addrACA subrr addr0 mulrDl -splitr. +Qed. + +End max_min. + +Notation trivial := (ltac:(done)). diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 9c39fd60b..59770fbc6 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -327,6 +327,9 @@ split=> [|[->|[r r0 ->//]]]; last by rewrite real_leey/=. by case: x => [r r0 | _ |//]; [right; exists r|left]. Qed. +Lemma fine0 : fine 0 = 0%R :> R. Proof. by []. Qed. +Lemma fine1 : fine 1 = 1%R :> R. Proof. by []. Qed. + End ERealOrder_numDomainType. #[global] Hint Resolve lee01 lte01 : core. diff --git a/theories/normedtype.v b/theories/normedtype.v index 4970e3caf..a8ddcbf8e 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -38,6 +38,12 @@ Require Import ereal reals signed topology prodnormedzmodule. (* ball_norm == balls defined by the norm. *) (* edist == the extended distance function for a *) (* pseudometric X, from X*X -> \bar R *) +(* edist_inf A == the infimum of distances to the set A *) +(* Urysohn A B == a continuous function T -> [0,1] which *) +(* separates A and B when *) +(* `uniform_separator A B` *) +(* uniform_separator A B == There is a suitable uniform space and *) +(* entourage separating A and B *) (* nbhs_norm == neighborhoods defined by the norm. *) (* closed_ball == closure of a ball. *) (* f @`[ a , b ], f @`] a , b [ == notations for images of intervals, *) @@ -2606,16 +2612,6 @@ End NbhsNorm. (* TODO: generalize to R : numFieldType *) Section hausdorff. -Lemma Rhausdorff (R : realFieldType) : hausdorff_space R. -Proof. -move=> x y clxy; apply/eqP; rewrite eq_le. -apply/in_segment_addgt0Pr => _ /posnumP[e]. -rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos. -have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he). -have := ball_triangle yz_he (ball_sym zx_he). -by rewrite -mulr2n -mulr_natr divfK // => /ltW. -Qed. - Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType) (V : pseudoMetricNormedZmodType R) : hausdorff_space V. @@ -3573,6 +3569,31 @@ Unshelve. all: end_near. Qed. End ecvg_realFieldType. +Section max_cts. +Context {R : realType} {T : topologicalType}. + +Lemma continuous_min (f g : T -> R^o) x : + {for x, continuous f} -> {for x, continuous g} -> + {for x, continuous (f \min g)}. +Proof. +move=> ctsf ctsg. +under [_ \min _]eq_fun => ? do rewrite minr_absE. +apply: cvgM; [|exact: cvg_cst]; apply:cvgD; first exact: cvgD. +by apply: cvgN; apply: cvg_norm; apply: cvgB. +Qed. + +Lemma continuous_max (f g : T -> R^o) x : + {for x, continuous f} -> {for x, continuous g} -> + {for x, continuous (f \max g)}. +Proof. +move=> ctsf ctsg. +under [_ \max _]eq_fun => ? do rewrite maxr_absE. +apply: cvgM; [|exact: cvg_cst]; apply:cvgD; first exact: cvgD. +by apply: cvg_norm; apply: cvgB. +Qed. + +End max_cts. + #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to cvgeN, and generalized to filter in Type")] Notation ereal_cvgN := cvgeN. @@ -3608,6 +3629,10 @@ by apply: lb_ereal_inf => z [+ []] => _/posnumP[r] _ <-; rewrite lee_fin. Qed. Hint Resolve edist_ge0 : core. +Lemma edist_neqNy (xy : X * X) : (edist xy != -oo)%E. +Proof. by rewrite -lteNye (@lt_le_trans _ _ 0%E). Qed. +Hint Resolve edist_neqNy : core. + Lemma edist_lt_ball r (xy : X * X) : (edist xy < r%:E)%E -> ball xy.1 r xy.2. Proof. case/ereal_inf_lt => ? [+ []] => _/posnumP[eps] bxye <-; rewrite lte_fin. @@ -3669,23 +3694,15 @@ Proof. by rewrite /edist /=; under eq_fun do rewrite ball_symE. Qed. Lemma edist_triangle (x y z : X) : (edist (x, z) <= edist (x, y) + edist (y, z))%E. Proof. +have [->|] := eqVneq (edist (x, y)) +oo%E; first by rewrite addye ?leey. +have [->|] := eqVneq (edist (y, z)) +oo%E; first by rewrite addey ?leey. +rewrite -?ltey -?ge0_fin_numE//. +move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. have [|] := eqVneq (edist (x, z)) +oo%E. - have [-> ->|] := eqVneq (edist (x, y)) +oo%E. - by rewrite addye ?lexx// -lteNye (lt_le_trans _ (edist_ge0 _)). - have [-> ? ->|] := eqVneq (edist (y, z)) +oo%E. - by rewrite addey ?lexx// -lteNye (lt_le_trans _ (edist_ge0 _)). - rewrite -?ltey -?ge0_fin_numE//. - move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. move/edist_pinftyP /(_ (r1%:num + r2%:num) _) => -[//|]. exact: (ball_triangle xy). rewrite -ltey -ge0_fin_numE// => /[dup] xzfin. move/edist_finP => [_/posnumP[del] /= xz]. -have [->|] := eqVneq (edist (x, y)) +oo%E. - by rewrite addye ?leey// -lteNye (lt_le_trans _ (edist_ge0 _)). -have [->|] := eqVneq (edist (y, z)) +oo%E. - by rewrite addey ?leey// -lteNye (lt_le_trans _ (edist_ge0 _)). -rewrite -?ltey -?ge0_fin_numE //. -move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy]. rewrite /edist /= ?ereal_inf_EFin; first last. - by exists (r1%:num + r2%:num); split => //; apply: (ball_triangle xy). - by exists 0 => ? /= [/ltW]. @@ -3705,66 +3722,499 @@ Qed. Lemma edist_continuous : continuous edist. Proof. -case=> x y; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. +move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xy | edist xy = +oo]%E). by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->. by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open. rewrite -ltey -ge0_fin_numE// => efin. rewrite -[edist (x, y)]fineK//; apply: cvg_EFin. by have := edist_fin_open efin; apply: filter_app; near=> w. -move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE. -move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=. -have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n. -exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)). - by split => //=; rewrite nbhs_ballE; - exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)). -case => a b /= [/ball_sym xar yar]; apply: distrU => /=. -have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E. - by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +apply/cvgrPdist_le => _/posnumP[eps]. +suff: \forall t \near (nbhs x, nbhs y), + `|fine (edist (x, y)) - fine (edist t)| <= eps%:num by []. +rewrite -near2_pair; near=> a b => /=. +have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E. + rewrite (edist_sym x a) -addeA. + by rewrite (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E. + rewrite (edist_sym y b) -addeA. + by rewrite (le_trans (@edist_triangle _ a _))// ?lee_add// ?edist_triangle. +have xafin : edist (x, a) \is a fin_num. + by apply/edist_finP; exists 1 =>//; near: a; apply: (nbhsx_ballx _ 1%:pos). +have ybfin : edist (y, b) \is a fin_num. + by apply/edist_finP; exists 1 =>//; near: b; apply: (nbhsx_ballx _ 1%:pos). have abfin : edist (a, b) \is a fin_num. - rewrite ge0_fin_numE// (le_lt_trans abxy)//. - by apply: lte_add_pinfty; [apply: lte_add_pinfty|]; - rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R). -have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num. - by rewrite abse_fin_num fin_numB abfin efin. -have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R). -have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4%:R). -rewrite -fineB// -fine_abse ?fin_numB ?abfin ?efin//. -rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. - rewrite fine_le// ?fin_numD ?daxr ?dybr//. - have [xyab|xyab] := leP (edist (a, b)) (edist (x, y)). - rewrite gee0_abs ?subre_ge0// lee_subl_addr//. - rewrite (le_trans (@edist_triangle _ a _))// (edist_sym a x) -addeA. - by rewrite lee_add// addeC (edist_sym y) edist_triangle. - rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC. - by rewrite lee_subl_addr// addeAC. -rewrite fineD // [_%:num]splitr. -have r42 : r%:num / 4%:R < r%:num / 2. - by rewrite ltr_pmul2l// ltf_pinv ?posrE ?ltr0n// ltr_nat. -by apply: ltr_add; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin. -Unshelve. end_near. Qed. + by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE. +have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num + by rewrite fin_numB abfin efin. +rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//. +rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first. + by rewrite [eps%:num]splitr/= EFinD lee_add//; apply: edist_fin => //=; + [near: a | near: b]; apply: (nbhsx_ballx _ (_ / _)%:pos). +have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)). + by rewrite gee0_abs ?subre_ge0// lee_subl_addr// addeAC. +rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//. +by rewrite addeC lee_subl_addr// addeAC. +Unshelve. all: end_near. Qed. Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E. Proof. -rewrite ball_close; split; first last. - by move=> edist0 eps; apply: (@edist_lt_ball _ (x, y)); rewrite edist0. -move=> bxy; apply: le_anti; rewrite edist_ge0 andbT leNgt; apply/negP => dpos. +rewrite ball_close; split=> [bxy|edist0 eps]; first last. + by apply: (@edist_lt_ball _ (x, y)); rewrite edist0. +case: ltgtP (edist_ge0 (x, y)) => // dpos _. have xxfin : edist (x, y) \is a fin_num. by rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin. -move: (dpos); rewrite -[edist _]fineK // lte_fin => dpose. +have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK. pose eps := PosNum dpose. have : (edist (x, y) <= (eps%:num / 2)%:E)%E. apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //. - exact: (bxy (@PosNum R (eps%:num / 2) ltac:(done))). -rewrite leNgt; move/negP; apply. + exact: (bxy (eps%:num / 2)%:pos). +apply: contra_leP => _. by rewrite /= EFinM fineK// lte_pdivr_mulr// lte_pmulr// lte1n. Qed. Lemma edist_refl x : edist (x, x) = 0%E. Proof. exact/edist_closeP. Qed. +Lemma edist_closel x y z : close x y -> edist (x, z) = edist (y, z). +Proof. +move=> /edist_closeP xy0; apply: le_anti; apply/andP; split. + by rewrite -[edist (y, z)]add0e -xy0 edist_triangle. +by rewrite -[edist (x, z)]add0e -xy0 [edist (x, y)]edist_sym edist_triangle. +Qed. + End pseudoMetricDist. #[global] -Hint Resolve edist_ge0 : core. +Hint Extern 0 (is_true (0 <= edist _)%E) => solve [apply: edist_ge0] : core. +#[global] +Hint Extern 0 (is_true (edist _ != -oo%E)) => solve [apply: edist_neqNy] : core. + +Section edist_inf. +Context {R : realType} {T : pseudoMetricType R} (A : set T). + +Definition edist_inf z := ereal_inf [set edist (z, a) | a in A]. + +Lemma edist_inf_ge0 w : (0 <= edist_inf w)%E. +Proof. by apply: lb_ereal_inf => ? /= [? ? <-]; exact: edist_ge0. Qed. +Hint Resolve edist_inf_ge0 : core. + +Lemma edist_inf_neqNy w : (edist_inf w != -oo)%E. +Proof. by rewrite -lteNye (@lt_le_trans _ _ 0%E). Qed. +Hint Resolve edist_inf_neqNy : core. + +Lemma edist_inf_triangle x y : (edist_inf x <= edist (x, y) + edist_inf y)%E. +Proof. +have [A0|/set0P[a0 Aa0]] := eqVneq A set0. + by rewrite /edist_inf A0 ?image_set0 ?ereal_inf0 addey. +have [fyn|] := boolP (edist_inf y \is a fin_num); first last. + by rewrite ge0_fin_numE// ?ltey// negbK => /eqP->; rewrite addey ?leey. +have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last. + by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey. +apply: lee_adde => eps. +have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn. +apply: le_trans; first by apply: (@ereal_inf_lb _ _ (edist (x, a))); exists a. +apply: le_trans; first exact: (@edist_triangle _ _ _ y). +by rewrite -addeA lee_add2lE // ltW. +Qed. + +Lemma edist_inf_continuous : continuous edist_inf. +Proof. +move=> z; have [A0|/= /set0P[a0 Aa0]] := eqVneq A set0. + rewrite /edist_inf A0 image_set0 ereal_inf0. + by under eq_fun => ? do rewrite image_set0 ereal_inf0; apply: cvg_cst. +have [] := eqVneq (edist_inf z) +oo%E. + move=> /[dup] fzp /ereal_inf_pinfty => zAp U /= Ufz. + have : nbhs z (ball z 1) by exact: nbhsx_ballx. + apply: filter_app; near_simpl; near=> w => bz1w. + suff /= -> : (edist_inf w) = +oo%E by apply: nbhs_singleton; rewrite -fzp. + apply/ereal_inf_pinfty => r [a Aa] war; apply/zAp; exists a => //. + have /gee0P[|[r' r'pos war']] := edist_ge0 (w, a). + by rewrite war => ->; apply: zAp; exists a. + have := @edist_triangle _ _ z w a; rewrite war'; apply: contra_leP => _. + rewrite (@le_lt_trans _ _ (1 + r'%:E)%E) ?lee_add2r ?edist_fin//. + by rewrite -EFinD [edist (z, a)]zAp ?ltey //; exists a. +rewrite -ltey -ge0_fin_numE ?edist_inf_ge0 // => fz_fin. +rewrite // -[edist_inf z]fineK //; apply/fine_cvgP. +have fwfin : \forall w \near z, edist_inf w \is a fin_num. + (have : nbhs z (ball z 1) by exact: nbhsx_ballx); apply: filter_app. + near=> t => bz1; rewrite ge0_fin_numE ?edist_inf_ge0 //. + rewrite (le_lt_trans (edist_inf_triangle _ z))//. + rewrite -ge0_fin_numE ?adde_ge0 ?edist_inf_ge0 //. + rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //. + exact/ball_sym. +split => //; apply/cvgrPdist_le => _/posnumP[eps]. +have : nbhs z (ball z eps%:num) by apply: nbhsx_ballx. +apply: filter_app; near_simpl; move: fwfin; apply: filter_app. +near=> t => tfin /= /[dup] ?. +have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num. +move=> /(@edist_fin _ _ _ (z, t)) - /(_ trivial). +rewrite -[edist (z, t)]fineK ?lee_fin //; apply: le_trans. +rewrite ler_norml; apply/andP; split. + rewrite ler_subr_addr addrC ler_subl_addr addrC -fineD //. + rewrite -lee_fin ?fineK // ?fin_numD ?ztfin ?fz_fin // edist_sym. + exact: edist_inf_triangle. +rewrite ler_subl_addr -fineD // -lee_fin ?fineK // ?fin_numD ?tfin ?ztfin //. +exact: edist_inf_triangle. +Unshelve. all: by end_near. Qed. + +Lemma edist_inf0 a : A a -> edist_inf a = 0%E. +Proof. +move=> Aa; apply: le_anti; apply/andP; split; last exact: edist_inf_ge0. +by apply: ereal_inf_lb; exists a => //; exact: edist_refl. +Qed. + +End edist_inf. +#[global] +Hint Extern 0 (is_true (0 <= edist_inf _ _)%E) => + solve [apply: edist_inf_ge0] : core. +#[global] +Hint Extern 0 (is_true (edist_inf _ _ != -oo%E)) => + solve [apply: edist_inf_neqNy] : core. + +Section urysohn_separator. +Context {T : uniformType} {R : realType}. +Context (A B : set T) (E : set (T * T)). +Hypothesis entE : entourage E. +Hypothesis AB0 : A `*` B `&` E = set0. + +Local Notation T' := (@gauge_pseudoMetricType _ _ entE R). + +Local Lemma urysohn_separation : exists (f : T -> R), + [/\ continuous f, range f `<=` `[0, 1], + f @` A `<=` [set 0] & f @` B `<=` [set 1] ]. +Proof. +have [eps exy] : exists (eps : {posnum R}), + forall (x y : T'), A x -> B y -> ~ ball x eps%:num y. + have : @entourage T' E by exists O => /=. + rewrite -entourage_ballE; case=> _/posnumP[eps] epsdiv; exists eps. + move=> x y Ax By bxy; have divxy := epsdiv (x, y) bxy. + by have : set0 (x, y) by rewrite -AB0; split. +have [->|/set0P[a A0]] := eqVneq A set0. + exists (fun=> 1); split; first by move => ?; exact: cvg_cst. + - by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //. + - by rewrite image_set0. + - by move=> ? [? ? <-]. +have dfin x : @edist_inf R T' A x \is a fin_num. + rewrite ge0_fin_numE ?edist_inf_ge0 //; apply: le_lt_trans. + by apply: ereal_inf_lb; exists a. + rewrite -ge0_fin_numE ?edist_ge0 //; apply/edist_finP => /=; exists 2 => //. + exact: countable_uniform_bounded. +pose f' := (fun z => fine (@edist_inf R T' A z)) \min (fun=> eps%:num). +pose f z := (f' z)/eps%:num; exists f; split. +- move=> x; rewrite /f; apply: (@cvgM R T (nbhs x)); last exact: cvg_cst. + suff : {for x, continuous (f' : T' -> R)}. + move=> Q U; rewrite nbhs_simpl /= => f'U. + have [J /(gauge_ent entE) entJ/filterS] := Q _ f'U; apply. + by rewrite nbhs_simpl /= -nbhs_entourageE /=; exists J. + apply: continuous_min; last by apply: cvg_cst; exact: nbhs_filter. + apply: fine_cvg; first exact: nbhs_filter. + rewrite fineK //; first exact: edist_inf_continuous. +- move=> _ [x _ <-]; rewrite set_itvE /=; apply/andP; split. + by rewrite /f divr_ge0 // /f' /= /minr; case: ltP; rewrite ?fine_ge0. + by rewrite /f ler_pdivr_mulr // mul1r /f' /= /minr; case: ltP => // /ltW. +- by move=> ? [z Az] <-; rewrite /f/f' /= edist_inf0 // /minr fine0 ifT ?mul0r. +- move=> ? [b Bb] <-; rewrite /f /f'/= /minr/=. + case: ltP => //; rewrite ?divrr // ?unitf_gt0 // -lte_fin fineK//. + move => /ereal_inf_lt [_ [z Az <-]] ebz; have [] := exy _ _ Az Bb. + exact/ball_sym/(@edist_lt_ball R T' _ (b, z)). +Qed. + +End urysohn_separator. + +Section topological_urysohn_separator. +Context {T : topologicalType} {R : realType}. + +Definition uniform_separator (A B : set T) := + exists (uT : @Uniform.class_of T^o) (E : set (T * T)), + let UT := Uniform.Pack uT in [/\ + @entourage UT E, A `*` B `&` E = set0 & + (forall x, @nbhs UT UT x `<=` @nbhs T T x)]. + +Local Lemma Urysohn' (A B : set T) : exists (f : T -> R), + [/\ continuous f, + range f `<=` `[0, 1] + & uniform_separator A B -> + f @` A `<=` [set 0] /\ f @` B `<=` [set 1]]. +Proof. +have [[? [E [entE ABE0 coarseT]]]|nP] := pselect (uniform_separator A B). + have [f] := @urysohn_separation _ R _ _ _ entE ABE0. + by case=> ctsf ? ? ?; exists f; split => // ? ? /= ?; apply/coarseT/ctsf. +exists (fun=>1); split => //; first by move=> ?; exact: cvg_cst. +by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //. +Qed. + +Definition Urysohn (A B : set T) : T -> R := projT1 (cid (Urysohn' A B)). + +Section urysohn_facts. + +Lemma Urysohn_continuous (A B : set T) : continuous (Urysohn A B). +Proof. by have [] := projT2 (cid (@Urysohn' A B)). Qed. + +Lemma Urysohn_range (A B : set T) : range (Urysohn A B) `<=` `[0, 1]. +Proof. by have [] := projT2 (cid (@Urysohn' A B)). Qed. + +Lemma Urysohn_sub0 (A B : set T) : + uniform_separator A B -> Urysohn A B @` A `<=` [set 0]. +Proof. by move=> eE; have [_ _ /(_ eE)[]] := projT2 (cid (@Urysohn' A B)). Qed. + +Lemma Urysohn_sub1 (A B : set T) : + uniform_separator A B -> Urysohn A B @` B `<=` [set 1]. +Proof. by move=> eE; have [_ _ /(_ eE)[]] := projT2 (cid (@Urysohn' A B)). Qed. + +Lemma Urysohn_eq0 (A B : set T) : + uniform_separator A B -> A !=set0 -> Urysohn A B @` A = [set 0]. +Proof. +move=> eE Aa; have [_ _ /(_ eE)[As0 _]] := projT2 (cid (@Urysohn' A B)). +rewrite eqEsubset; split => // ? ->; case: Aa => a ?; exists a => //. +by apply: As0; exists a. +Qed. + +Lemma Urysohn_eq1 (A B : set T) : + uniform_separator A B -> (B !=set0) -> (Urysohn A B) @` B = [set 1]. +Proof. +move=> eE Bb; have [_ _ /(_ eE)[_ Bs0]] := projT2 (cid (@Urysohn' A B)). +rewrite eqEsubset; split => // ? ->; case: Bb => b ?; exists b => //. +by apply: Bs0; exists b. +Qed. + +End urysohn_facts. +End topological_urysohn_separator. + +Lemma uniform_separatorW {T : uniformType} (A B : set T) : + (exists2 E, entourage E & A `*` B `&` E = set0) -> + uniform_separator A B. +Proof. by case=> E entE AB0; exists (Uniform.class T), E; split => // ?. Qed. + +Section Urysohn. +Context {T : topologicalType} . +Hypothesis normalT : normal_space T. +Section normal_uniform_separators. +Context (A : set T). + +Local Notation "A ^-1" := [set xy | A (xy.2, xy.1)] : classical_set_scope. + +Local Notation "'to_set' A x" := [set y | A (x, y)] + (at level 0, A at level 0) : classical_set_scope. + +(* Urysohn's lemma guarantees a continuous function : T -> R + where "f @` A = [set 0]" and "f @` B = [set 1]". + The idea is to leverage countable_uniformity to build that function + rather than construct it directly. + + The bulk of the work is building a uniformity to measure "distance from A". + Each pair of "nested" U,V induces an approxmiantion "apxU". + A-------)] U + A----------------) V (points near A) + (------------ ~`closure U (points far from A) + These make the sub-basis for a filter. That filter is a uniformity + because normality lets us split + + A------)] U + A-----------)] V' + (--------------- ~`closure U + A----------------) V + (--------- ~` closure V' + and (U,V') + (V', V) splits the entourage of (U,V). This uniform space is not + neccesarily a pseudometric. So we find an entourage which divides A and B, + then the gauge pseudometric gives us what we want. +*) + +Let apxU (UV : set T * set T) : set (T * T) := + (UV.2 `*` UV.2) `|` (~` closure UV.1 `*` ~` closure UV.1). + +Let nested (UV : set T * set T) := + [/\ open UV.1, open UV.2, A `<=` UV.1 & closure UV.1 `<=`UV.2]. + +Let ury_base := [set apxU UV | UV in nested]. + +Local Lemma ury_base_refl E : + ury_base E -> [set fg | fg.1 = fg.2] `<=` E. +Proof. +case; case=> L R [_ _ _ /= LR] <- [? x /= ->]. +case: (pselect (R x)); first by left. +by move/subsetC: LR => /[apply] => ?; right. +Qed. + +Local Lemma ury_base_inv E : ury_base E -> ury_base (E^-1)%classic. +Proof. +case; case=> L R ? <-; exists (L, R) => //. +by rewrite eqEsubset; split => //; (case=> x y [] [? ?]; [left| right]). +Qed. + +Local Lemma ury_base_split E : ury_base E -> + exists E1 E2, [/\ ury_base E1, ury_base E2 & + (E1 `&` E2) \; (E1 `&` E2) `<=` E]. +Proof. +case; case => L R [/= oL oR AL cLR <-]. +have [R' []] : exists R', [/\ open R', closure L `<=` R' & closure R' `<=` R]. + have := @normalT (closure L) (@closed_closure T L). + case/(_ R); first by move=> x /cLR ?; apply: open_nbhs_nbhs. + move=> V /set_nbhsP [U] [? ? ? cVR]; exists U; split => //. + by apply: (subset_trans _ cVR); exact: closure_subset. +move=> oR' cLR' cR'R; exists (apxU (L, R')), (apxU (R', R)). +split; first by exists (L, R'). + exists (R', R) => //; split => //; apply: (subset_trans AL). + by apply: (subset_trans _ cLR'); exact: subset_closure. +case=> x z /= [y [+ +] []]. +(do 4 (case; case=> /= ? ?)); try (by left); try (by right); + match goal with nG : (~ closure ?S ?y), G : ?S ?y |- _ => + by move/subset_closure: G + end. +Qed. + +Let ury_unif := smallest Filter ury_base. + +Instance ury_unif_filter : Filter ury_unif. +Proof. exact: smallest_filter_filter. Qed. + +Local Lemma ury_unif_refl E : ury_unif E -> [set fg | fg.1 = fg.2] `<=` E. +Proof. +move/(_ (globally [set fg | fg.1 = fg.2])); apply; split. + exact: globally_filter. +exact: ury_base_refl. +Qed. + +Local Lemma set_prod_invK (K : set (T * T)) : (K^-1^-1)%classic = K. +Proof. by rewrite eqEsubset; split; case. Qed. + +Local Lemma ury_unif_inv E : ury_unif E -> ury_unif (E^-1)%classic. +Proof. +move=> ufE F [/filter_inv FF urF]; have [] := ufE [set (V^-1)%classic | V in F]. + split => // K /ury_base_inv/urF /= ?; exists (K^-1)%classic => //. + by rewrite set_prod_invK. +by move=> R FR <-; rewrite set_prod_invK. +Qed. + +Local Lemma ury_unif_split_iter E n : + filterI_iter ury_base n E -> exists2 K : set (T * T), + filterI_iter ury_base n.+1 K & K\;K `<=` E. +Proof. +elim: n E; first move=> E []. +- move=> ->; exists setT => //; exists setT; first by left. + by exists setT; rewrite ?setIT; first by left. +- move=> /[dup] /ury_base_split [E1 [E2] [? ? ? ?]]; exists (E1 `&` E2) => //. + by (exists E1; first by right); exists E2; first by right. +move=> n IH E /= [E1 /IH [F1 F1n1 F1E1]] [E2 /IH [F2 F2n1 F2E2]] E12E. +exists (F1 `&` F2); first by exists F1 => //; exists F2. +move=> /= [x z ] [y /= [K1xy K2xy] [K1yz K2yz]]; rewrite -E12E; split. + by apply: F1E1; exists y. +by apply: F2E2; exists y. +Qed. + +Local Lemma ury_unif_split E : ury_unif E -> + exists2 K, ury_unif K & K \; K `<=` E. +Proof. +rewrite /ury_unif filterI_iterE; case=> G [n _] /ury_unif_split_iter []. +move=> K SnK KG GE; exists K; first by exists K => //; exists n.+1. +exact: (subset_trans _ GE). +Qed. + +Local Lemma ury_unif_covA E : ury_unif E -> A `*` A `<=` E. +Proof. +rewrite /ury_unif filterI_iterE; case=> G [n _] sG /(subset_trans _); apply. +elim: n G sG. + move=> g [-> //| [[P Q]]] [/= _ _ AP cPQ <-] [x y] [/= /AP ? ?]. + by left; split => //=; apply/cPQ/subset_closure => //; exact: AP. +by move=> n IH G [R] /IH AAR [M] /IH AAM <- z; split; [exact: AAR | exact: AAM]. +Qed. + +Let urysohn_uniformType_mixin := + UniformMixin ury_unif_filter ury_unif_refl ury_unif_inv ury_unif_split erefl. + +Let urysohn_topologicalTypeMixin := + topologyOfEntourageMixin urysohn_uniformType_mixin. + +Let urysohn_filtered := FilteredType T T (nbhs_ ury_unif). +Let urysohn_topologicalType := + TopologicalType urysohn_filtered urysohn_topologicalTypeMixin. +Let urysohn_uniformType := UniformType + urysohn_topologicalType urysohn_uniformType_mixin. + +Lemma normal_uniform_separator (B : set T) : + closed A -> closed B -> A `&` B = set0 -> uniform_separator A B. +Proof. +move=> clA clB AB0; have /(_ (~`B))[x Ax|] := normalT clA. + apply: open_nbhs_nbhs; split => //. + - exact/closed_openC. + - by move: x Ax; apply/ disjoints_subset. +move=> V /set_nbhsP [U [oU AU UV]] cVcb. +exists (Uniform.class urysohn_uniformType), (apxU (U, ~` B)); split => //. +- move=> ?; apply:sub_gen_smallest; exists (U, ~`B) => //; split => //=. + exact/closed_openC. + by move: UV => /closure_subset/subset_trans; apply. +- rewrite eqEsubset; split; case=> // a b [/=[Aa Bb] [[//]|]]. + by have /subset_closure ? := AU _ Aa; case. +move=> x ? [E gE] /(@filterS T); apply; move: gE. +rewrite /ury_unif filterI_iterE; case => K /= [i _] /= uiK KE. +suff : @nbhs T T x to_set K (x) by apply: filterS => y /KE. +elim: i K uiK {E KE}; last by move=> ? H ? [N] /H ? [M] /H ? <-; apply: filterI. +move=> K [->|]; first exact: filterT. +move=> [[/= P Q] [/= oP oQ AP cPQ <-]]; rewrite /apxU /=. +set M := [set y | _ \/ _]. +have [Qx|nQx] := pselect (Q x); first last. + suff -> : M = ~` closure P. + apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure. + by move/cPQ. + rewrite eqEsubset /M; split => z; first by do 2!case. + by move=> ?; right; split => // /cPQ. +have [nPx|cPx] := pselect (closure P x). + suff -> : M = Q by apply: open_nbhs_nbhs; split. + rewrite eqEsubset /M; split => z; first by do 2!case. + by move=> ?; left; split. +suff -> : M = setT by exact: filterT. +rewrite eqEsubset; split => // z _. +by have [Qz|/(subsetC cPQ)] := pselect (Q z); constructor. +Qed. + +End normal_uniform_separators. +End Urysohn. + +Lemma uniform_separatorP {T : topologicalType} {R : realType} (A B : set T) : + uniform_separator A B <-> + exists (f : T -> R), [/\ continuous f, range f `<=` `[0, 1], + f @` A `<=` [set 0] & f @` B `<=` [set 1]]. +Proof. +split; first do [move=> ?; exists (Urysohn A B); split]. +- exact: Urysohn_continuous. +- exact: Urysohn_range. +- exact: Urysohn_sub0. +- exact: Urysohn_sub1. +case=> f [ctsf f01 fA0 fB1]; pose T' := weak_pseudoMetricType f. +exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split. +- exists [set xy | ball xy.1 1 xy.2]; last by case. + by rewrite -entourage_ballE; exists 1 => //=. +- rewrite -subset0 => -[a b [[/= Aa Bb]]]. + by rewrite (imsub1 fA0)// (imsub1 fB1)// /ball/= sub0r normrN normr1 ltxx. +- move=> x U [V [[W oW <- /=]]] ? /filterS; apply; apply: ctsf. + exact: open_nbhs_nbhs. +Qed. + +Lemma normal_urysohnP {T : topologicalType} {R : realType} : + normal_space T <-> + forall (A B : set T), closed A -> closed B -> + A `&` B = set0 -> uniform_separator A B. +Proof. +split; first by move=> *; exact: normal_uniform_separator. +move=> + A clA B /set_nbhsP [C [oC AC CB]]. +have AC0 : A `&` ~` C = set0 by apply/disjoints_subset; rewrite setCK. +move=> /(_ _ _ clA (open_closedC oC) AC0). +move=> /(@uniform_separatorP _ R) [f [cf f01 fa0 fc1]]. +exists (f@^-1` `]-1, 1/2]). + apply (@filterS _ _ _ (f @^-1` (`]-1, 1/2[))). + by apply: preimage_subset; first exact: subset_itvW. + apply/set_nbhsP; exists (f @^-1` `]-1, 1/2[); split => //. + by apply: open_comp => //; exact: interval_open. + by rewrite set_itvoo=> x Ax /=; rewrite (imsub1 fa0)//; apply/andP; split. +have -> : f @^-1` `]-1, 1/2] = f @^-1` `[0, 1/2]. + rewrite eqEsubset set_itvcc set_itvoc; split. + by move=> x /= /andP [_ ->]; rewrite (itvP (f01 _ _)). + by apply: preimage_subset => z /= /andP[z0 ->]; rewrite (lt_le_trans _ z0). +have: closed (f @^-1` `[0, 1/2]) + by apply: closed_comp => //; apply: interval_closed. +rewrite closure_id => <-. +apply: (subset_trans _ CB); apply/subsetCP. +rewrite preimage_setC set_itvcc => x nCx /=; apply/negP. +by rewrite (imsub1 fc1)// ler01/= -ltNge [ltRHS]splitr ltr_addr. +Qed. Section open_closed_sets_ereal. Variable R : realFieldType (* TODO: generalize to numFieldType? *). @@ -4814,7 +5264,7 @@ move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b -> have [| |c cab /oppr_inj] := ivt (- f) (- v); last by exists c. - by move=> x; apply: continuousN; apply: fcont. - by rewrite ler_oppr opprK ler_oppr opprK andbC. -move=> favfb; suff: is_interval (f @` `[a,b]). +move=> favfb; suff: is_interval (f @` `[a, b]). apply; last exact: favfb. - by exists a => //=; rewrite in_itv/= lexx. - by exists b => //=; rewrite in_itv/= leab lexx. @@ -5179,9 +5629,9 @@ rewrite normfZV ?subr_eq0// mulr1 normrM (gtr0_norm s0) gtr0_norm //. by rewrite ltr_pdivr_mulr // ltr_pmulr // ltr1n. Qed. -Lemma closed_ball_closed (R : realFieldType) (V : normedModType R) (x : V) - (r : R) : 0 < r -> closed (closed_ball x r). -Proof. by move => r0; rewrite closed_ballE //; exact: closed_closed_ball_. Qed. +Lemma closed_ball_closed (R : realFieldType) (V : pseudoMetricType R) (x : V) + (r : R) : closed (closed_ball x r). +Proof. exact: closed_closure. Qed. Lemma closed_ballR_compact (R : realType) (x e : R) : 0 < e -> compact (closed_ball x e). @@ -5208,9 +5658,9 @@ apply: (subset_trans (closed_ball_subset _ _) xrB) => //=. by rewrite lter_pdivr_mulr // ltr_pmulr // ltr1n. Qed. -Lemma subset_closed_ball (R : realFieldType) (V : normedModType R) (x : V) - (r : R) : 0 < r -> ball x r `<=` closed_ball x r. -Proof. move=> r0; rewrite /closed_ball; apply: subset_closure. Qed. +Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V) + (r : R) : ball x r `<=` closed_ball x r. +Proof. exact: subset_closure. Qed. Lemma locally_compactR (R : realType) : locally_compact [set: R]. Proof. @@ -5219,6 +5669,14 @@ move=> x _; rewrite withinET; exists (closed_ball x 1). by split; [apply: closed_ballR_compact | apply: closed_ball_closed]. Qed. +Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V) + (r : R) : 0 < r -> closed_ball x (r/2) `<=` ball x r. +Proof. +move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. + exact: nbhsx_ballx. +by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle. +Qed. + (*TBA topology.v once ball_normE is there*) Lemma interior_closed_ballE (R : realType) (V : normedModType R) (x : V) @@ -5231,7 +5689,7 @@ have [-> _|nxt] := eqVneq t x; first exact: ballxx. near ((0 : R^o)^') => e; rewrite -ball_normE /closed_ball_ => tsxr. pose z := t + `|e| *: (t - x); have /tsxr /= : `|t - z| < s. rewrite distrC addrAC subrr add0r normrZ normr_id. - rewrite -ltr_pdivl_mulr ?(normr_gt0,subr_eq0) //. + rewrite -ltr_pdivl_mulr ?(normr_gt0, subr_eq0) //. by near: e; apply/dnbhs0_lt; rewrite divr_gt0 // normr_gt0 subr_eq0. rewrite /z opprD addrA -scalerN -{1}(scale1r (x - t)) opprB -scalerDl normrZ. apply lt_le_trans; rewrite ltr_pmull; last by rewrite normr_gt0 subr_eq0 eq_sym. diff --git a/theories/topology.v b/theories/topology.v index 530a9e145..8fd9776a7 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -117,6 +117,7 @@ Require Import reals signed. (* predicates on natural numbers that are *) (* eventually true. *) (* clopen U == U is both open and closed *) +(* normal_space X == X is normal, sometimes called T4 *) (* separate_points_from_closed f == For a closed set U and point x outside *) (* some member of the family f sends *) (* f_i(x) outside (closure (f_i @` U)). *) @@ -1573,14 +1574,14 @@ apply: filter_from_filter. by exists F; split => //; exists setT; exact: filterT. move=> M N /= [entM subM [M0 MM0]] [entN subN [N0 NN0]]. exists [set E | exists P Q, [/\ M P, N Q & E = P `&` Q] ]; first split. -- by move=> ? [? [? [? ? ->]]]; apply filterI; [exact: entM | exact: entN]. +- by move=> ? [? [? [? ? ->]]]; apply: filterI; [exact: entM | exact: entN]. - move=> ? E2 [P [Q [MP MQ ->]]] entE2 E2subPQ; exists E2, E2. split; last by rewrite setIid. + by apply: (subM _ _ MP) => // ? /E2subPQ []. + by apply: (subN _ _ MQ) => // ? /E2subPQ []. - by exists (M0 `&` N0), M0, N0. - move=> E /= [P [Q [MP MQ ->]]]; have entPQ : F (P `&` Q). - by apply filterI; [exact: entM | exact: entN]. + by apply: filterI; [exact: entM | exact: entN]. by split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)] => // ? []. Qed. @@ -1999,6 +2000,7 @@ exact: (near (withinT A FF) w). Unshelve. all: by end_near. Qed. End within_topologicalType. + Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). (** ** Topology defined by a filter *) @@ -2745,8 +2747,8 @@ Lemma continuous_closedP (S T : topologicalType) (f : S -> T) : continuous f <-> forall A, closed A -> closed (f @^-1` A). Proof. rewrite continuousP; split=> ctsf ? ?. - by rewrite -openC preimage_setC; apply ctsf; rewrite openC. -by rewrite -closedC preimage_setC; apply ctsf; rewrite closedC. + by rewrite -openC preimage_setC; apply: ctsf; rewrite openC. +by rewrite -closedC preimage_setC; apply: ctsf; rewrite closedC. Qed. Lemma closedU (T : topologicalType) (D E : set T) : @@ -2834,7 +2836,7 @@ rewrite predeqE => p; have PF : ProperFilter F by []. split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first. by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI. exists (filter_from (\bigcup_(A in F) [set A `&` B | B in nbhs p]) id). - apply filter_from_proper; last first. + apply: filter_from_proper; last first. by move=> _ [A FA [B p_B <-]]; have := clFp _ _ FA p_B. apply: filter_from_filter. exists setT; exists setT; first exact: filterT. @@ -2941,7 +2943,7 @@ have /locK : forall x, K x -> move=> x Kx; have : ~ cluster F x. by apply: contraPnot KclstF0 => clstFx; apply/eqP/set0P; exists x. move=> /existsNP [U /existsNP [V /not_implyP [FU /not_implyP [nbhsV]]]] UV0. - near=> x' W => //= => Wx'; apply UV0; exists x'. + near=> x' W => //= => Wx'; apply: UV0; exists x'. by split; [exact: (near (small_set_sub FU) W) | exact: (near nbhsV x')]. case=> G [GF Gdown [U GU]] GP; apply: (@filterS _ _ _ U); last exact: GF. by move=> y Uy Ky; exact: (GP _ GU y Ky). @@ -3017,7 +3019,7 @@ suff UAF : ProperFilter (\bigcup_(H in A) projT1 H). by move=> B FB; exists G => //; apply: sFG. exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=. by exists H. -apply Build_ProperFilter. +apply: Build_ProperFilter. by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF). split; first by exists G => //; apply: filterT. move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC. @@ -3059,7 +3061,7 @@ Qed. Lemma proper_image (T U : Type) (f : T -> U) (F : set (set T)) : ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | A in F]. Proof. -move=> FF fsurj; apply Build_ProperFilter; last exact: filter_image. +move=> FF fsurj; apply: Build_ProperFilter; last exact: filter_image. by move=> _ [A FA <-]; have /filter_ex [p Ap] := FA; exists (f p); exists p. Qed. @@ -3079,7 +3081,7 @@ move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right. left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id). move=> /max_filter <-; last by move=> B FB; exists B => //; left. by exists A => //; right; exists setT; [apply: filterT|rewrite setIT]. -apply filter_from_proper; last first. +apply: filter_from_proper; last first. move=> B [|[C FC <-]]; first exact: filter_ex. apply: contrapT => /asboolP; rewrite asbool_neg => /forallp_asboolPn AC0. by apply: nFnA; apply: filterS FC => p Cp Ap; apply: (AC0 p). @@ -3252,7 +3254,7 @@ apply: (@filterS _ _ _ ((dfwith g i) @^-1` V)); first by exists V. have [L Lsub /[dup] VL <-] := QfinP _ JV; rewrite preimage_bigcap. apply: filter_bigI => /= M /[dup] LM /Lsub /set_mem [] w _ [+] + /[dup] + <-. have [->|wnx] := eqVneq w i => N oN NM. - apply (@filterS _ _ _ N); first by move=> ? ?; rewrite /= dfwithin. + apply: (@filterS _ _ _ N); first by move=> ? ?; rewrite /= dfwithin. apply: open_nbhs_nbhs; split => //; move: Vpz. by rewrite -VL => /(_ _ LM); rewrite -NM /= dfwithin. apply: nearW => y /=; move: Vpz. @@ -3644,7 +3646,7 @@ Lemma connectedPn A : ~ connected A <-> exists E : bool -> set T, [/\ forall b, E b !=set0, A = E false `|` E true & separated (E false) (E true)]. Proof. -rewrite -propeqE; apply notLR; rewrite propeqE. +rewrite -propeqE; apply: notLR; rewrite propeqE. split=> [conE [E [E0 EU [E1 E2]]]|conE B B0 [C oC BAC] [D cD BAD]]. suff : E true = A. move/esym/(congr1 (setD^~ (closure (E true)))); rewrite EU setDUl. @@ -3855,7 +3857,7 @@ by rewrite openE => ? ?; rewrite /interior dsc; exact/principal_filterP. Qed. Lemma discrete_set1 (x : X) : nbhs x [set x]. -Proof. by apply open_nbhs_nbhs; split => //; exact: discrete_open. Qed. +Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed. Lemma discrete_closed (A : set X) : closed A. Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed. @@ -4127,7 +4129,7 @@ Program Definition topologyOfEntourageMixin (T : Type) Topological.mixin_of nbhs := topologyOfFilterMixin _ _ _. Next Obligation. move=> T nbhsT m p. -rewrite (Uniform.nbhsE m) nbhs_E; apply filter_from_proper; last first. +rewrite (Uniform.nbhsE m) nbhs_E; apply: filter_from_proper; last first. by move=> A entA; exists p; apply: Uniform.entourage_refl entA _ _. apply: filter_from_filter. by exists setT; apply: @filterT (Uniform.entourage_filter m). @@ -4165,10 +4167,20 @@ Definition nbhs_simpl := (nbhs_simpl,@filter_from_entourageE,@nbhs_entourageE). End NbhsEntourage. -Lemma nbhsP {M : uniformType} (x : M) P : - nbhs x P <-> nbhs_ entourage x P. +Lemma nbhsP {M : uniformType} (x : M) P : nbhs x P <-> nbhs_ entourage x P. Proof. by rewrite nbhs_simpl. Qed. +Lemma filter_inv {T : Type} (F : set (set (T * T))) : + Filter F -> Filter [set (V^-1)%classic | V in F]. +Proof. +move=> FF; split => /=. +- by exists [set: T * T] => //; exact: filterT. +- by move=> P Q [R FR <-] [S FS <-]; exists (R `&` S) => //; exact: filterI. +- move=> P Q PQ [R FR RP]; exists Q^-1%classic => //; first last. + by rewrite eqEsubset; split; case. + by apply: filterS FR; case=> ? ? /= ?; apply: PQ; rewrite -RP. +Qed. + Section uniformType1. Context {M : uniformType}. @@ -4719,7 +4731,7 @@ rewrite predeq2E => x V; split. rewrite -subTset => ??; apply: BV; exists (\bigcap_(i in [set` F]) i) => //. by move=> w /Fsup/set_mem; rewrite /sup_subbase I0 bigcup_set0. have f : forall w, {p : IEnt | w \in F -> to_set ((projT1 p).2) x `<=` w}. - move=> /= v; apply cid; case (pselect (v \in F)); first last. + move=> /= v; apply: cid; case (pselect (v \in F)); first last. by move=> ?; exists (exist ent_of _ (IEnt_pointT i0)). move=> /[dup] /Fx vx /Fsup/set_mem [i _]; rewrite openE => /(_ x vx). by move=> /(@nbhsP (TS i)) [w /asboolP ent ?]; exists (exist _ (i, w) ent). @@ -4766,7 +4778,7 @@ exists (finI_from (\bigcup_n g n) id); split. - by apply/finI_from_countable/bigcup_countable => //i _; case: (projT2 (f i)). - move=> E [A AsubGn AE]; exists E => //. have h (w : set (T * T)) : { p : IEnt | w \in A -> w = (projT1 p).2 }. - apply cid; have [|] := boolP (w \in A); last first. + apply: cid; have [|] := boolP (w \in A); last first. by exists (exist ent_of _ (IEnt_pointT i0)). move=> /[dup] /AsubGn /set_mem [n _ gnw] wA. suff ent : ent_of (n, w) by exists (exist ent_of (n, w) ent). @@ -5698,11 +5710,11 @@ Qed. Global Instance ball_filter (R : realFieldType) (t : R) : Filter [set P | exists2 i : R, 0 < i & ball_ Num.norm t i `<=` P]. Proof. -apply Build_Filter; [by exists 1 | move=> P Q | move=> P Q PQ]; rewrite /mkset. +apply: Build_Filter; [by exists 1 | move=> P Q | move=> P Q PQ]; rewrite /mkset. - move=> -[x x0 xP] [y ? yQ]; exists (Num.min x y); first by rewrite lt_minr x0. move=> z tz; split. - by apply xP; rewrite /= (lt_le_trans tz) // le_minl lexx. - by apply yQ; rewrite /= (lt_le_trans tz) // le_minl lexx orbT. + by apply: xP; rewrite /= (lt_le_trans tz) // le_minl lexx. + by apply: yQ; rewrite /= (lt_le_trans tz) // le_minl lexx orbT. - by move=> -[x ? xP]; exists x => //; apply: (subset_trans xP). Qed. @@ -6100,6 +6112,16 @@ rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. by rewrite {2}(splitr e%:num) ltr_spaddl. Qed. +Lemma Rhausdorff (R : realFieldType) : hausdorff_space R. +Proof. +move=> x y clxy; apply/eqP; rewrite eq_le. +apply/in_segment_addgt0Pr => _ /posnumP[e]. +rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos. +have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he). +have := ball_triangle yz_he (ball_sym zx_he). +by rewrite -mulr2n -mulr_natr divfK // => /ltW. +Qed. + Section RestrictedUniformTopology. Context {U : choiceType} (A : set U) {V : uniformType} . @@ -6253,7 +6275,7 @@ move=> FF; split. - move=> cvgF P' /= /uniform_nbhs [ E [/= entE EsubP]]. apply: (filterS EsubP); apply: cvgF => /=. apply: (filterS ( P:= [set h | forall y, A y -> E(f y, h y)])). - + by move=> h/= Eh [y ?] _; apply Eh; rewrite -inE. + + by move=> h/= Eh [y ?] _; apply: Eh; rewrite -inE. + by (apply/uniform_nbhs; eexists; split; eauto). - move=> cvgF P' /= /uniform_nbhs [ E [/= entE EsubP]]. apply: (filterS EsubP). @@ -6323,19 +6345,19 @@ apply: (filterS EsubQ). rewrite (_: [set h | (forall y : U, (A `|` B) y -> E (f y, h y))] = [set h | forall y, A y -> E (f y, h y)] `&` [set h | forall y, B y -> E (f y, h y)]). -- apply filterI; [apply: AFf| apply: BFf]. +- apply: filterI; [apply: AFf| apply: BFf]. + by apply/uniform_nbhs; exists E; split. + by apply/uniform_nbhs; exists E; split. - rewrite eqEsubset; split=> h. - + by move=> R; split=> t ?; apply R;[left| right]. - + by move=> [R1 R2] y [? | ?]; [apply R1| apply R2]. + + by move=> R; split=> t ?; apply: R;[left| right]. + + by move=> [R1 R2] y [? | ?]; [apply: R1| apply: R2]. Qed. Lemma cvg_uniform_set0 (F : set (set (U -> V))) (f : U -> V) : Filter F -> {uniform set0, F --> f}. Proof. move=> FF P /= /uniform_nbhs [E [? R]]. -suff -> : P = setT by apply filterT. +suff -> : P = setT by exact: filterT. rewrite eqEsubset; split => //=. by apply: subset_trans R => g _ ?. Qed. @@ -6648,7 +6670,7 @@ by rewrite le_floor// lef_pinv ?invrK ?invr_gt0//; exact: (lt_le_trans _ e1e2). Qed. Local Fixpoint n_step_ball n x e z := - if n is S n then exists y d1 d2, + if n is n.+1 then exists y d1 d2, [/\ n_step_ball n x d1 y, 0 < d1, 0 < d2, @@ -6819,10 +6841,8 @@ move=> l ln1 Ox1x4. case: (@split_n_step_ball l x1 (N.+1%:R^-1/2) (N.+1%:R^-1/2) x4) => //. by rewrite -splitr. move=> x2 [x3] [l1] [l2] [] P1 [? +] P3 l1l2; rewrite -splitr distN_nat => ?. -have l1n : (l1 <= n)%N. - by apply (leq_trans (leq_addr l2 l1)); rewrite l1l2 -ltnS. -have l2n : (l2 <= n)%N. - by apply (leq_trans (leq_addl l1 l2)); rewrite l1l2 -ltnS. +have l1n : (l1 <= n)%N by rewrite (leq_trans (leq_addr l2 l1))// l1l2 -ltnS. +have l2n : (l2 <= n)%N by rewrite (leq_trans (leq_addl l1 l2))// l1l2 -ltnS. apply: splitG3; exists x3; [exists x2 => //|]. by move/(n_step_ball_le (distN_half N))/(IH1 _ l1n) : P1. by move/(n_step_ball_le (distN_half N))/(IH1 _ l2n) : P3. @@ -6842,10 +6862,20 @@ apply: (subset_trans _ fN); apply: subset_trans; last apply: gsubf. by case=> x y /= N1ball; apply: (@subset_step_ball x N.+1). Qed. -(* Note this is the only non-local result from this section *) +(* Note these are the only non-local result from this section *) Definition countable_uniform_pseudoMetricType_mixin := PseudoMetric.Mixin step_ball_center step_ball_sym step_ball_triangle step_ball_entourage. +Lemma countable_uniform_bounded (x y : T) : + let U := PseudoMetricType _ countable_uniform_pseudoMetricType_mixin + in @ball _ U x 2 y. +Proof. +rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN. +suff -> : @floor R 2^-1 = 0 by rewrite absz0 /=. +apply/eqP; rewrite -[_ == _]negbK; rewrite floor_neq0 negb_or -?ltNge -?leNgt. +by apply/andP; split => //; rewrite invf_lt1 //= ltr_addl. +Qed. + End countable_uniform. Section sup_pseudometric. @@ -7098,7 +7128,7 @@ have/closure_id <- := (closed_subspaceT) => /setIidr <-; rewrite setIC. move=> UsubA; rewrite eqEsubset; split. apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U). by apply: closed_subspaceW; exact: closed_closure. -rewrite -VAclUA; apply setSI; rewrite closureE //=; apply: smallest_sub => //. +rewrite -VAclUA; apply: setSI; rewrite closureE //=; apply: smallest_sub => //. apply: subset_trans (@subIsetl _ V A); rewrite VAclUA subsetI; split => //. exact: (@subset_closure _ (U : set (subspace A))). Qed. @@ -7198,7 +7228,7 @@ Lemma continuous_in_subspaceT {U} A (f : T -> U) : {in A, continuous f} -> {within A, continuous f}. Proof. rewrite continuous_subspace_in ?in_setP => ctsf t At. -by apply continuous_subspaceT_for => //=; apply: ctsf. +by apply: continuous_subspaceT_for => //=; apply: ctsf. Qed. Lemma continuous_subspaceT {U} A (f : T -> U) : @@ -7293,12 +7323,12 @@ move=> ?; case=> E entE Esub. exists [set xy | xy.1 = xy.2 \/ A xy.1 /\ A xy.2 /\ split_ent E xy]. by exists (split_ent E). move=> [x y] [z /= Ez zE] /=; case: Ez; case: zE. - - by move=> -> ->; apply Esub; left. - - move=> [ ? []] ? G xy; subst; apply Esub; right; repeat split => //=. + - by move=> -> ->; apply: Esub; left. + - move=> [ ? []] ? G xy; subst; apply: Esub; right; repeat split => //=. by apply: entourage_split => //=; first exact: G; exact: entourage_refl. - - move=> -> [ ? []] ? G; apply Esub; right; repeat split => //=. + - move=> -> [ ? []] ? G; apply: Esub; right; repeat split => //=. by apply: entourage_split => //=; first exact: G; exact: entourage_refl. - - move=> []? []? ?[]?[]??; apply Esub; right; repeat split => //=. + - move=> []? []? ?[]?[]??; apply: Esub; right; repeat split => //=. by apply: subset_split_ent => //; exists z. Qed. Next Obligation. @@ -7490,14 +7520,14 @@ move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy. have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP. move=> i P; suff : join_product x i != join_product y i by rewrite jxjy => /eqP. apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. -by apply subset_closure; exists y. +by apply: subset_closure; exists y. Qed. Lemma join_product_weak : set_inj [set: T] join_product -> @open T = @open (weak_topologicalType join_product). Proof. move=> inj; rewrite predeqE => U; split; first last. - by move=> [V ? <-]; apply open_comp => // + _; exact: join_product_continuous. + by move=> [V ? <-]; apply: open_comp => // + _; exact: join_product_continuous. move=> /join_product_open/open_subspaceP [V [oU VU]]. exists V => //; have := @f_equal _ _ (preimage join_product) _ _ VU. rewrite !preimage_setI // !preimage_range !setIT => ->. @@ -7528,7 +7558,7 @@ Lemma connected_continuous_connected (T U : topologicalType) (A : set T) (f : T -> U) : connected A -> {within A, continuous f} -> connected (f @` A). Proof. -move=> cA cf; apply contrapT => /connectedPn[E [E0 fAE sE]]. +move=> cA cf; apply: contrapT => /connectedPn[E [E0 fAE sE]]. set AfE := fun b =>(A `&` f @^-1` E b) : set (subspace A). suff sAfE : separated (AfE false) (AfE true). move: cA; apply/connectedPn; exists AfE; split; last (rewrite /AfE; split). @@ -7548,7 +7578,7 @@ have [fAfE cEIE] : split; last by case: sE => ? ?; case: b => //; rewrite setIC. rewrite eqEsubset; split => [|u Ebu]. apply: (subset_trans sub_image_setI). - by apply subIset; right; exact: image_preimage_subset. + by apply: subIset; right; exact: image_preimage_subset. have [t [At ftu]] : exists t, A t /\ f t = u. suff [t At ftu] : (f @` A) u by exists t. by rewrite fAE; case: b Ebu; [left|right]. @@ -7564,7 +7594,7 @@ have ? : f @` closure (AfE b) `<=` closure (E b). apply/eqP/negPn/negP/set0P => -[t [? ?]]. have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0. by rewrite fAfE; exact: subsetI_eq0 cEIE. -by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply fcAfEb; split; exists t. +by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t. Qed. Lemma uniform_limit_continuous {U : topologicalType} {V : uniformType} @@ -7763,6 +7793,10 @@ Qed. End gauges. +Definition normal_space (T : topologicalType) := + forall (A : set T), closed A -> + set_nbhs A `<=` filter_from (set_nbhs A) closure. + Section ArzelaAscoli. Context {X : topologicalType}. Context {Y : uniformType}. @@ -7831,7 +7865,7 @@ apply: (subclosed_compact _ C); first exact: closed_closure. have WsubR : (fW @` W) `<=` R. move=> f Wf x; rewrite /R /K closure_limit_point; left. by case: Wf => i ? <-; exists i. -rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR. +rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR. exact: hausdorff_product. Qed. @@ -7896,7 +7930,7 @@ move=> FW ectsW; split=> [ptwsF|]; last exact: pointwise_cvg_compact_family. apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [eE EsubU]]]. suff : \forall g \near within W (nbhs f), forall y, K y -> E (f y, g y). rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW). - by apply ptwsF; near=> g => ?; apply EsubU; apply: (near N g). + by apply: ptwsF; near=> g => ?; apply: EsubU; apply: (near N g). near (powerset_filter_from (@entourage Y)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). pose Q := fun (h : X -> Y) x => E' (f x, h x). @@ -7963,7 +7997,7 @@ apply: (entourage_split (f y) (entourage_split_ent entE)). apply: (near (small_ent_sub _) E') => //. by near: y; apply: ((@ctsW f Wf x) (to_set _ _)); exact: nbhs_entourage. apply: (near (small_ent_sub _) E') => //. -by apply (near (fam_nbhs _ entE' cptU) g) => //; exact: (near UWx y). +by apply: (near (fam_nbhs _ entE' cptU) g) => //; exact: (near UWx y). Unshelve. all: end_near. Qed. Lemma precompact_equicontinuous (W : set {family compact, X -> Y}) : @@ -7971,7 +8005,7 @@ Lemma precompact_equicontinuous (W : set {family compact, X -> Y}) : precompact (W : set {family compact, X -> Y}) -> equicontinuous W id. Proof. -move=> pcptW ctsW; apply (equicontinuous_subset_id (@subset_closure _ W)). +move=> pcptW ctsW; apply: (equicontinuous_subset_id (@subset_closure _ W)). apply: compact_equicontinuous; last by rewrite -precompactE. move=> f; rewrite closureEcvg => [[G PG [Gf GW]]] x B /=. rewrite -nbhs_entourageE => -[E entE] /filterS; apply; near_simpl.