Skip to content

Commit 40cbfa2

Browse files
zstone1zstone1
committed
docs and changelog
1 parent 515f2e6 commit 40cbfa2

File tree

2 files changed

+52
-65
lines changed

2 files changed

+52
-65
lines changed

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,10 +93,14 @@
9393
- in `classical_sets.v`:
9494
+ lemma `bigcup_bigcup`
9595

96-
- in file `normedtype.v`,
96+
+ new definitions `edist_inf`, `Urysohn`, and `Urysohn_normal`.
9797
+ new lemmas `maxr_absE`, `minr_absE`, `continuous_min`,
98-
`continuous_max`, `urysohn_seperation`, `normal_separatorsP`, and
99-
`subset_closure_half`.
98+
`continuous_max`, `edist_closel`, `edist_inf_ge0`, `edist_inf_triangle`,
99+
`edist_inf_continuous`, `edist_inf0`, `Urysohn_continuous`,
100+
`Urysohn_range`, `Urysohn_sub0`, `Urysohn_sub1`, `Urysohn_eq0`,
101+
`Urysohn_eq1`, `Urysohn_normal_continuous`, `Urysohn_normal_range`,
102+
`Urysohn_normal_sub0`, `Urysohn_normal_sub1`, `Urysohn_normal_eq0`,
103+
`Urysohn_normal_eq1`, `normal_urysohnP`, and `subset_closure_half`.
100104

101105
- in file `topology.v`,
102106
+ new definition `normal_space`.

‎theories/normedtype.v‎

Lines changed: 45 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,13 @@ Require Import ereal reals signed topology prodnormedzmodule.
3838
(* ball_norm == balls defined by the norm. *)
3939
(* edist == the extended distance function for a *)
4040
(* pseudometric X, from X*X -> \bar R *)
41+
(* edist_inf A == the infimum of distances to the set A *)
42+
(* Urysohn A B == a continuous function T -> [0,1] which *)
43+
(* separates A and B when there is an *)
44+
(* entourage separating them *)
45+
(* Urysohn_normal A B == a continuous function T -> [0,1] which *)
46+
(* separates A and B in a normal space *)
47+
(* when closure A `&` closure B = set0 *)
4148
(* nbhs_norm == neighborhoods defined by the norm. *)
4249
(* closed_ball == closure of a ball. *)
4350
(* f @`[ a , b ], f @`] a , b [ == notations for images of intervals, *)
@@ -3811,7 +3818,7 @@ End pseudoMetricDist.
38113818
#[global]
38123819
Hint Resolve edist_ge0 : core.
38133820

3814-
Section edist_set.
3821+
Section edist_inf.
38153822
Context {R : realType} {T : pseudoMetricType R} (A : set T).
38163823

38173824
Definition edist_inf z := ereal_inf [set edist (z, a) | a in A].
@@ -3835,32 +3842,27 @@ move=> fyn; case: (pselect (edist (x,y) \is a fin_num)); first last.
38353842
move/eqP=> ->; rewrite addeC addey ?leey // -ltNye.
38363843
exact: (lt_le_trans _(edist_inf_ge0 _)).
38373844
move=> xyfin; apply: lee_adde => eps.
3838-
have := !! @lb_ereal_inf_adherent R _ eps%:num (ltac:(done)) fyn.
3839-
case=> ? [a Aa <-] yaeps; apply: ltW; apply: le_lt_trans.
3840-
by apply: (@ereal_inf_lb _ _ (edist (x,a))); exists a.
3841-
apply: le_lt_trans.
3842-
apply: (@edist_triangle _ _ _ y).
3843-
rewrite -addeA lte_add2lE //.
3845+
have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn.
3846+
apply: le_trans; first by apply: (@ereal_inf_lb _ _ (edist (x,a))); exists a.
3847+
apply: le_trans; first exact: (@edist_triangle _ _ _ y).
3848+
by rewrite -addeA lee_add2lE //; exact: ltW.
38443849
Qed.
38453850

38463851
Lemma edist_inf_continuous : continuous edist_inf.
38473852
Proof.
38483853
move=> z; case : (pselect (A=set0)).
38493854
move=> A0; rewrite /edist_inf A0 image_set0 ereal_inf0.
3850-
under eq_fun => ? do rewrite image_set0 ereal_inf0.
3851-
exact: cvg_cst.
3852-
case/eqP/set0P => a0 Aa0.
3853-
case: (pselect (edist_inf z = +oo)%E).
3855+
by (under eq_fun => ? do rewrite image_set0 ereal_inf0); exact: cvg_cst.
3856+
case/eqP/set0P => a0 Aa0; case: (pselect (edist_inf z = +oo)%E).
38543857
move=> /[dup] fzp; move/ereal_inf_pinfty=> zAp U /= Ufz.
38553858
have : nbhs z (ball z 1) by exact: nbhsx_ballx.
38563859
apply: filter_app; near_simpl; near=> w => bz1w.
3857-
suff /= -> : (edist_inf w) = +oo%E.
3858-
by apply: nbhs_singleton; rewrite -fzp.
3860+
suff /= -> : (edist_inf w) = +oo%E by apply: nbhs_singleton; rewrite -fzp.
38593861
apply/ereal_inf_pinfty => r [a Aa] war; apply/zAp; exists a => //.
3860-
case/gee0P: (edist_ge0 (w,a)); first by rewrite -war => ->; apply: zAp; exists a.
3861-
case=> r' r'pos => war'; apply/asboolP.
3862-
have := (@edist_triangle _ _ z w a); rewrite war'; apply: contra_leT => _.
3863-
apply: le_lt_trans.
3862+
case/gee0P: (edist_ge0 (w,a)).
3863+
by rewrite -war => ->; apply: zAp; exists a.
3864+
case=> r' r'pos => war'; apply/asboolP; have := (@edist_triangle _ _ z w a).
3865+
rewrite war'; apply: contra_leT => _; apply: le_lt_trans.
38643866
by apply: lee_add2r; apply (@edist_fin _ _ _ (z,w) ltr01 bz1w).
38653867
by rewrite -EFinD [edist (z,a)]zAp ?ltey //; exists a.
38663868
move/eqP; rewrite -ltey -ge0_fin_numE ?edist_inf_ge0 // => fz_fin.
@@ -3880,29 +3882,25 @@ have ztfin : edist (z,t) \is a fin_num by apply/edist_finP; exists eps%:num.
38803882
move=> /(@edist_fin _ _ _ (z,t)) => /(_ (ltac:(done))).
38813883
rewrite -[edist (z,t)]fineK ?lee_fin //.
38823884
move/(le_trans _); apply; rewrite ler_norml; apply/andP; split.
3883-
rewrite ler_subr_addr addrC ler_subl_addr addrC -fineD // -lee_fin ?fineK // ?fin_numD.
3884-
by rewrite edist_sym; exact: edist_inf_triangle.
3885-
by rewrite fz_fin ztfin.
3886-
rewrite ler_subl_addr -fineD // -lee_fin ?fineK // ?fin_numD.
3885+
rewrite ler_subr_addr addrC ler_subl_addr addrC -fineD //.
3886+
rewrite -lee_fin ?fineK // ?fin_numD ?ztfin ?fz_fin // edist_sym.
38873887
exact: edist_inf_triangle.
3888-
by rewrite tfin ztfin.
3888+
rewrite ler_subl_addr -fineD // -lee_fin ?fineK // ?fin_numD ?tfin ?ztfin //.
3889+
exact: edist_inf_triangle.
38893890
Unshelve. all: by end_near. Qed.
38903891

38913892
Lemma edist_inf0 a : A a -> edist_inf a = 0%E.
38923893
Proof.
3893-
move=> Aa; apply: le_anti; apply/andP.
3894-
split; last exact: edist_inf_ge0.
3894+
move=> Aa; apply: le_anti; apply/andP; split; last exact: edist_inf_ge0.
38953895
by apply: ereal_inf_lb; exists a => //; exact: edist_refl.
38963896
Qed.
38973897

3898-
End edist_set.
3898+
End edist_inf.
38993899

39003900
Section urysohn_separator.
39013901
Context {T : uniformType} {R : realType}.
39023902
Section urysohn_separator_full.
39033903
Context (A B : set T) (E : set (T * T)).
3904-
Hypothesis An0 : A !=set0.
3905-
Hypothesis Bn0 : B !=set0.
39063904
Hypothesis entE : entourage E.
39073905
Hypothesis AB0 : A `*` B `&` E = set0.
39083906

@@ -3917,14 +3915,17 @@ split=> // x y Ax By bxy; have divxy := epsdiv (x, y) bxy.
39173915
by (suff : (set0 (x,y)) by exact); rewrite -AB0; split.
39183916
Qed.
39193917

3920-
Local Lemma urysohn_separation:
3921-
exists (f : T -> R), [/\ continuous f,
3922-
f @` A = [set 0], f @` B = [set 1] & range f `<=` `[0,1]].
3918+
Local Lemma urysohn_separation: exists (f : T -> R), [/\ continuous f,
3919+
f @` A `<=` [set 0], f @` B `<=` [set 1] & range f `<=` `[0,1]].
39233920
Proof.
3924-
case: An0 => a Aa; pose eps' := projT1 (cid divide_eps).
3921+
case: (pselect (A = set0)); last case/eqP/set0P => a A0.
3922+
move=> ->; exists (fun=> 1); split; first by move => ?; exact: cvg_cst.
3923+
- by rewrite image_set0.
3924+
- by move=> ? [? ? <-].
3925+
- by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
3926+
pose eps' := projT1 (cid divide_eps).
39253927
have epos : 0 < eps' by case : (projT2 (cid divide_eps)).
3926-
pose eps := PosNum epos.
3927-
have dfin x : @edist_inf R T' A x \is a fin_num.
3928+
pose eps := PosNum epos; have dfin x : @edist_inf R T' A x \is a fin_num.
39283929
rewrite ge0_fin_numE ?edist_inf_ge0 //; apply: le_lt_trans.
39293930
by apply: ereal_inf_lb; exists a.
39303931
rewrite -ge0_fin_numE ?edist_ge0 //; apply/edist_finP => /=; exists 2 => //.
@@ -3939,18 +3940,8 @@ pose f z := (f' z)/eps%:num; exists f; split.
39393940
apply: continuous_min; last by apply: cvg_cst; exact: nbhs_filter.
39403941
apply: fine_cvg; first exact: nbhs_filter.
39413942
rewrite fineK //; first exact: edist_inf_continuous.
3942-
- rewrite eqEsubset /f /f' /=; split => ? /=.
3943-
by case=> z Az; rewrite edist_inf0 //= => <-; rewrite /minr epos mul0r.
3944-
by move=> ->; exists a => //; rewrite edist_inf0 //= /minr epos mul0r.
3945-
- rewrite eqEsubset /f /f' /=; split => ?; first last.
3946-
move=> ->; case: Bn0 => b Bb; exists b => //; rewrite /minr.
3947-
case P: (fine (_ _) < eps'); rewrite ?divrr // ?unitf_gt0 //.
3948-
move: P; rewrite ltNge => /negP; apply: absurd.
3949-
rewrite -lee_fin fineK // leNgt; apply/negP => /ereal_inf_lt.
3950-
case=> ? [z Az <-] => ebz.
3951-
have [_ /(_ _ _ Az Bb)] := projT2 (cid divide_eps); apply.
3952-
by apply: (@edist_lt_ball R T' _ (z:T',b:T')); rewrite edist_sym.
3953-
case=> b Bb; rewrite /minr.
3943+
- by move=> ? [z Az] <-; rewrite /f/f' /= edist_inf0 // /minr epos mul0r.
3944+
- move=> ? [b Bb] <- ; rewrite/f/f'/= /minr /=.
39543945
case P: (fine (_ _) < eps'); rewrite ?divrr // ?unitf_gt0 //.
39553946
move: P; rewrite ltNge => /negP; apply: absurd.
39563947
rewrite -lee_fin fineK // leNgt; apply/negP => /ereal_inf_lt.
@@ -3972,16 +3963,8 @@ Local Lemma Urysohn' (A B : set T):
39723963
& (exists2 E, entourage E & A `*` B `&` E = set0) ->
39733964
f @` A `<=` [set 0] /\ f @` B `<=` [set 1]].
39743965
Proof.
3975-
case: (pselect (A = set0)); last move/eqP/set0P=> A0.
3976-
move=> ->; exists (fun=>1); split => //; first by move=> ?; exact: cvg_cst.
3977-
by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
3978-
by move=> _; split; rewrite ?image_set0 // => ? [] ? _ <-.
3979-
case: (pselect (B = set0)); last move/eqP/set0P=> B0.
3980-
move=> ->; exists (fun=>0); split => //; first by move=> ?; exact: cvg_cst.
3981-
by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
3982-
by move=> _; split; rewrite ?image_set0 // => ? [] ? _ <-.
39833966
case: (pselect (exists2 E, entourage E & A `*` B `&` E = set0)).
3984-
case => E entE ABE0; have [f] := urysohn_separation A0 B0 entE ABE0.
3967+
case => E entE ABE0; have [f] := urysohn_separation entE ABE0.
39853968
by case=> ? fA fB ?; exists f; split => // _; split; rewrite ?fA ?fB.
39863969
move=> nP; exists (fun=>1); split => //; first by move=> ?; exact: cvg_cst.
39873970
by move=> ? [? _ <-]; rewrite /= in_itv /=; apply/andP; split => //.
@@ -4064,7 +4047,7 @@ Local Notation "'to_set' A x" := ([set y | A (x, y)])
40644047
Local Definition apxU (UV : set T * set T) : set (T * T) :=
40654048
(UV.2 `*` UV.2) `|` (~` closure UV.1 `*` ~` closure UV.1).
40664049

4067-
Let nested (UV : set T * set T) :=
4050+
Local Definition nested (UV : set T * set T) :=
40684051
[/\ open UV.1, open UV.2, A `<=` UV.1 & closure UV.1 `<=`UV.2].
40694052

40704053
Local Definition ury_base := [set apxU UV | UV in nested].
@@ -4104,7 +4087,7 @@ case=> x z /= [y [+ +] []].
41044087
end.
41054088
Qed.
41064089

4107-
Let ury_unif := smallest Filter ury_base.
4090+
Local Definition ury_unif := smallest Filter ury_base.
41084091

41094092
Instance ury_unif_filter : Filter ury_unif.
41104093
Proof. exact: smallest_filter_filter. Qed.
@@ -4218,7 +4201,7 @@ Qed.
42184201
End normal_uniform_separators.
42194202
Context {R : realType}.
42204203

4221-
Definition Urysohn_normal (A B : set T) : T -> R :=
4204+
Definition Urysohn_normal (A B : set T) : T -> R :=
42224205
@Urysohn (urysohn_uniformType (closure A)) R (closure A) (closure B).
42234206

42244207
Section urysohn_normal_facts.
@@ -4233,23 +4216,23 @@ Lemma Urysohn_normal_sub0 (A B : set T) :
42334216
closure A `&` closure B = set0 ->
42344217
(Urysohn_normal A B) @` closure A `<=` [set 0].
42354218
Proof.
4236-
move=> clAB; apply: (@Urysohn_sub0 (urysohn_uniformType (closure A))).
4219+
move=> clAB; apply: (@Urysohn_sub0 (urysohn_uniformType (closure A))).
42374220
apply: normal_entourage_separator => //; exact: closed_closure.
42384221
Qed.
42394222

42404223
Lemma Urysohn_normal_sub1 (A B : set T) :
42414224
closure A `&` closure B = set0 ->
42424225
(Urysohn_normal A B) @` closure B `<=` [set 1].
42434226
Proof.
4244-
move=> clAB; apply: (@Urysohn_sub1 (urysohn_uniformType (closure A))).
4227+
move=> clAB; apply: (@Urysohn_sub1 (urysohn_uniformType (closure A))).
42454228
apply: normal_entourage_separator => //; exact: closed_closure.
42464229
Qed.
42474230

42484231
Lemma Urysohn_normal_eq0 (A B : set T) :
42494232
closure A `&` closure B = set0 ->
42504233
(A !=set0) -> (Urysohn_normal A B) @` closure A = [set 0].
42514234
Proof.
4252-
move=> clAB A0; apply: (@Urysohn_eq0 (urysohn_uniformType (closure A))).
4235+
move=> clAB A0; apply: (@Urysohn_eq0 (urysohn_uniformType (closure A))).
42534236
by apply: normal_entourage_separator => //; exact: closed_closure.
42544237
by apply: (subset_nonempty _ A0); exact: subset_closure.
42554238
Qed.
@@ -4258,7 +4241,7 @@ Lemma Urysohn_normal_eq1 (A B : set T) :
42584241
closure A `&` closure B = set0 ->
42594242
(B !=set0) -> (Urysohn_normal A B) @` closure B = [set 1].
42604243
Proof.
4261-
move=> clAB B0; apply: (@Urysohn_eq1 (urysohn_uniformType (closure A))).
4244+
move=> clAB B0; apply: (@Urysohn_eq1 (urysohn_uniformType (closure A))).
42624245
by apply: normal_entourage_separator => //; exact: closed_closure.
42634246
by apply: (subset_nonempty _ B0); exact: subset_closure.
42644247
Qed.
@@ -4272,7 +4255,7 @@ Lemma normal_urysohnP {T : topologicalType} {R : realType} :
42724255
f @` A `<=` [set 0], f @` B `<=` [set 1] & range f `<=` `[0,1]]).
42734256
Proof.
42744257
split.
4275-
move=> nT A B /closure_id -> /closure_id -> AB0.
4258+
move=> nT A B /closure_id -> /closure_id -> AB0.
42764259
exists (Urysohn_normal nT A B); split => //.
42774260
- exact: Urysohn_normal_continuous.
42784261
- exact: Urysohn_normal_sub0.

0 commit comments

Comments
 (0)