Files

Module mathcomp.analysis.normedtype_theory.urysohn

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum interval.
From mathcomp Require Import interval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions set_interval.
From mathcomp Require Import reals.
From mathcomp Require Import topology ereal edist num_normedtype normed_module.

# Urysohn's lemma ``` uniform_separator A B == there is a suitable uniform space and entourage separating A and B Urysohn A B == a continuous function T -> [0,1] which separates A and B when `uniform_separator A B` completely_regular_space == a space where points and closed sets can be separated by a function into R completely_regular_uniformity == equips a completely_regular_space with the uniformity induced by continuous functions into the reals note this uniformity is always the only choice, so its placed in a module ```

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section urysohn_separator.
Context {TSource code : uniformType} {RSource code : realType}.
Context (ASource code BSource code : set T) (ESource code : set (T * T)).
Hypothesis entESource code : entourage E.
Hypothesis AB0Source code : A `*` B `&` E = set0.

Local Notation T'Source code := [the pseudoMetricType R of gauge.type entE].

Local Lemma urysohn_separationSource code : exists (fSource code : T -> R),
  [/\ continuous f, range f `<=` `[0, 1],
      f @` A `<=` [set 0] & f @` B `<=` [set 1] ].
Proof.
have [eps exy] : exists (epsSource code : {posnum R}),
    forall (xSource code ySource code : 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 (cst 1); split; first exact: cst_continuous.
  - 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_lbound; exists a.
  rewrite -ge0_fin_numE ?edist_ge0 //; apply/edist_finP => /=; exists 2 => //.
  exact: countable_uniform.countable_uniform_bounded.
pose f' := (fun zSource code => fine (@edist_inf R T' A z)) \min (fun=> eps%:num).
pose f zSource code := (f' z)/eps%:num; exists f; split.
- move=> x; rewrite /f; apply: (@cvgM R T (nbhs x)) => //.
  suff : {for x, continuous (f' : T' -> R)}.
    move=> Q U; rewrite nbhs_simpl /= => f'U.
    have [J /(gauge.gauge_ent entE) entJ/filterS] := Q _ f'U; apply.
    by rewrite nbhs_simpl /= -nbhs_entourageE /=; exists J.
  apply: continuous_min; last exact: cst_continuous.
  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' /= le_min fine_ge0//= edist_inf_ge0.
  by rewrite /f ler_pdivrMr // mul1r /f' /= ge_min lexx orbT.
- by move=> ? [z Az] <-; rewrite /f/f' /= edist_inf0 // fine0 min_l// mul0r.
- move=> ? [b Bb] <-; rewrite /f /f'/=; case: ltP; rewrite ?divff//.
  rewrite -lte_fin fineK// => /ereal_inf_lt [_ [z Az <-]] ebz.
  by have [] := exy _ _ Az Bb; exact/ball_sym/(@edist_lt_ball R T' _ (b, z)).
Qed.

End urysohn_separator.

Section topological_urysohn_separator.
Context {TSource code : topologicalType} {RSource code : realType}.

Definition uniform_separator

uniform_separator : forall {T : topologicalType}, set T -> set T -> Prop uniform_separator is not universe polymorphic Arguments uniform_separator {T} (A B)%_classical_set_scope uniform_separator is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.urysohn.uniform_separator Declared in library mathcomp.analysis.normedtype_theory.urysohn, line 93, characters 11-28

Source code (ASource code BSource code : set T) :=
  exists (uTSource code : @Uniform.axioms_ T^o) (ESource code : set (T * T)),
    let UTSource code := Uniform.Pack uT in [/\
      @entourage UT E, A `*` B `&` E = set0 &
      (forall xSource code, @nbhs UT UT x `<=` @nbhs T T x)].

Local Lemma Urysohn'Source code (ASource code BSource code : set T) : exists (fSource code : 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 => // ? ? /= ?; exact/coarseT/ctsf.
exists (cst 1); split => //; first exact: cst_continuous.
by move=> ? [? _ <-]/=; rewrite bound_itvE.
Qed.

Definition Urysohn

Urysohn : forall {T : topologicalType} {R : realType}, set T -> set T -> T -> R Urysohn is not universe polymorphic Arguments Urysohn {T R} (A B)%_classical_set_scope _ Urysohn is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.urysohn.Urysohn Declared in library mathcomp.analysis.normedtype_theory.urysohn, line 112, characters 11-18

Source code (ASource code BSource code : set T) : T -> R := projT1 (cid (Urysohn' A B)).

Section urysohn_facts.

Lemma Urysohn_continuousSource code (ASource code BSource code : set T) : continuous (Urysohn A B).
Proof.
by have [] := projT2 (cid (@Urysohn' A B)). Qed.

Lemma Urysohn_rangeSource code (ASource code BSource code : set T) : range (Urysohn A B) `<=` `[0, 1].
Proof.
by have [] := projT2 (cid (@Urysohn' A B)). Qed.

Lemma Urysohn_sub0Source code (ASource code BSource code : 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_sub1Source code (ASource code BSource code : 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_eq0Source code (ASource code BSource code : 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_eq1Source code (ASource code BSource code : 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_separatorWSource code {TSource code : uniformType} (ASource code BSource code : set T) :
    (exists2 ESource code, 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.
Local Open Scope relation_scope.
Context {TSource code : topologicalType}.
Hypothesis normalTSource code : normal_space T.
Section normal_uniform_separators.
Context (ASource code : set T).


Let apxUSource code (UVSource code : set T * set T) : set (T * T) :=
  (UV.2 `*` UV.2) `|` (~` closure UV.1 `*` ~` closure UV.1).

Let nestedSource code (UVSource code : set T * set T) :=
  [/\ open UV.1, open UV.2, A `<=` UV.1 & closure UV.1 `<=`UV.2].

Let ury_baseSource code := [set apxU UV | UVSource code in nested].

Local Lemma ury_base_reflSource code ESource code : ury_base E -> diagonal `<=` E.
Proof.
case; case=> L R [_ _ _ /= LR] <- [? x /= /diagonalP ->].
case: (pselect (R x)); first by left.
by move/subsetC: LR => /[apply] => ?; right.
Qed.

Local Lemma ury_base_invSource code ESource code : ury_base E -> ury_base E^-1.
Proof.
case; case=> L R ? <-; exists (L, R) => //.
by rewrite eqEsubset; split => //; (case=> x y [] [? ?]; [left| right]).
Qed.

Local Lemma ury_base_splitSource code ESource code : ury_base E ->
  exists E1Source code E2Source code, [/\ ury_base E1, ury_base E2 &
                    (E1 `&` E2) \; (E1 `&` E2) `<=` E].
Proof.
case; case => L R [/= oL oR AL cLR <-].
have [R' []] : exists R'Source code, [/\ 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: closureS.
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_unifSource code := smallest Filter ury_base.

Instance ury_unif_filterSource code : Filter ury_unif.
Proof.
exact: smallest_filter_filter. Qed.

Local Lemma ury_unif_reflSource code ESource code : ury_unif E -> diagonal `<=` E.
Proof.
by move/(_ (globally diagonal)); apply; split;
  [exact: globally_filter|exact: ury_base_refl].
Qed.

Local Lemma ury_unif_invSource code ESource code : ury_unif E -> ury_unif E^-1.
Proof.
move=> ufE F [/filter_inv FF urF]; have [] := ufE [set V^-1 | VSource code 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_iterSource code ESource code nSource code :
  filterI_iter ury_base n E -> exists2 KSource code : 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_splitSource code ESource code : ury_unif E ->
  exists2 KSource code, 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_covASource code ESource code : 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.

Definition urysohnType

urysohnType : topologicalType -> Type urysohnType is not universe polymorphic Arguments urysohnType {T} urysohnType is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.urysohn.urysohnType Declared in library mathcomp.analysis.normedtype_theory.urysohn, line 278, characters 11-22

Source code : Type := T.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code ChoiceSource code.on urysohnType.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code
  isUniform.Build urysohnType ury_unif_filter ury_unif_refl ury_unif_inv
  ury_unif_split.
HBSource code.instanceSource code DefinitionSource code _Source code {pSource code :Source code PointedSource code T} := Pointed.copy urysohnType (Pointed.Pack p).

Lemma normal_uniform_separatorSource code (BSource code : 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 urysohnType), (apxU (U, ~` B)); split => //.
- move=> ?; apply:sub_gen_smallest; exists (U, ~`B) => //; split => //=.
    exact/closed_openC.
  by move: UV => /closureS/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 [set ySource code | K (x, y)] by apply: filterS => y /KE/xsectionP.
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 ySource code | _ \/ _].
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_separatorPUsed by
  • mathcomp.analysis.numfun
Source code {TSource code : topologicalType} {RSource code : realType} (ASource code BSource code : set T) :
  uniform_separator A B <->
  exists (fSource code : 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' : uniformType := initial_topology f.
exists (Uniform.class T'), ([set xySource code | ball (f xy.1) 1 (f xy.2)]); split.
- exists [set xySource code | 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.
  by apply: ctsf; exact: open_nbhs_nbhs.
Qed.

Section normalP.
Context {RSource code : realType} {TSource code : topologicalType}.

Let normal_spacePSource code : [<->
normal_space T;
forall (ASource code BSource code : set T), closed A -> closed B -> A `&` B = set0 ->
    uniform_separator A B;
forall (ASource code BSource code : set T), closed A -> closed B -> A `&` B = set0 ->
    exists USource code VSource code, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0] ].
Proof.
tfae; first by move=> ?; exact: normal_uniform_separator.
- move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R).
  case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1].
  exists (f@^-1` `]-1, 1/2[), (f @^-1` `]1/2, 2[); split.
  + by apply: open_comp; [|exact: interval_open].
  + by apply: open_comp; [|exact: interval_open].
  + by apply: fa0 => x/= ->; rewrite (@in_itv _ R)/=; apply/andP; split.
  + apply: fb1 => x/= ->; rewrite (@in_itv _ R)/= ltr_pdivrMr// mul1r.
    by rewrite ltr1n.
  + rewrite -preimage_setI ?set_itvoo -subset0 => t [] /andP [_ +] /andP [+ _].
    by move=> /lt_trans /[apply]; rewrite ltxx.
move=> + A clA B /set_nbhsP [C [oC AC CB]].
have AC0 : A `&` ~` C = set0 by apply/disjoints_subset; rewrite setCK.
case/(_ _ _ clA (open_closedC oC) AC0) => U [V] [oU oV AU nCV UV0].
exists (~` closure V).
  apply/set_nbhsP; exists U; split => //.
  apply/subsetCr; have := open_closedC oU; rewrite closure_id => ->.
  by apply/closureS/disjoints_subset; rewrite setIC.
apply/(subset_trans _ CB)/subsetCP; apply: (subset_trans nCV).
apply/subsetCr; have := open_closedC oV; rewrite closure_id => ->.
exact/closureS/subsetC/subset_closure.
Qed.

Lemma normal_openPSource code : normal_space T <->
  forall (ASource code BSource code : set T), closed A -> closed B -> A `&` B = set0 ->
  exists USource code VSource code, [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0].
Proof.
exact: (normal_spaceP 0%N 2%N). Qed.

Lemma normal_separatorPUsed by
  • mathcomp.analysis.numfun
Source code : normal_space T <->
  forall (ASource code BSource code : set T), closed A -> closed B -> A `&` B = set0 ->
  uniform_separator A B.
Proof.
exact: (normal_spaceP 0%N 1%N). Qed.

End normalP.

Section completely_regular.
Context {RSource code : realType}.

This is equivalent to uniformizable. Note there is a subtle distinction between being uniformizable and being uniformType. There is often more than one possible uniformity, and being a uniformType has a specific one. If you don't care, you can use the `completely_regular_uniformity.type` which builds the uniformity.
Definition completely_regular_space

completely_regular_space : topologicalType -> Prop completely_regular_space is not universe polymorphic Arguments completely_regular_space T completely_regular_space is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.urysohn.completely_regular_space Declared in library mathcomp.analysis.normedtype_theory.urysohn, line 405, characters 11-35

Source code (TSource code : topologicalType) :=
  forall (aSource code : T) (BSource code : set T), closed B -> ~ B a -> uniform_separator [set a] B.

Lemma point_uniform_separatorSource code {TSource code : uniformType} (xSource code : T) (BSource code : set T) :
  closed B -> ~ B x -> uniform_separator [set x] B.
Proof.
move=> clB nBx; have : open (~` B) by rewrite openC.
rewrite openE => /(_ _ nBx); rewrite /interior /= -nbhs_entourageE.
case=> E entE EnB.
pose T' : pseudoMetricType R := gauge.type entE.
exists (Uniform.class T); exists E; split => //; last by move => ?.
by rewrite -subset0 => -[? w [/= [-> ? /xsectionP ?]]]; exact: (EnB w).
Qed.

Lemma uniform_completely_regularSource code {TSource code : uniformType} :
  @completely_regular_space T.
Proof.
by move=> x B clB Bx; exact: point_uniform_separator. Qed.

Lemma normal_completely_regularSource code {TSource code : topologicalType} :
  normal_space T -> accessible_space T -> completely_regular_space T.
Proof.
move/normal_separatorP => + /accessible_closed_set1 cl1 x A ? ?; apply => //.
by apply/disjoints_subset => ? ->.
Qed.

Lemma uniform_regularSource code {XSource code : uniformType} : @regular_space X.
Proof.
move=> x A; rewrite /= -nbhs_entourageE => -[E entE].
move/(subset_trans (ent_closure entE)) => ExA.
by exists (xsection (split_ent E) x) => //; exists (split_ent E).
Qed.

End completely_regular.

Module completely_regular_uniformitySource code.
Section completely_regular_uniformity.
Context {RSource code : realType} {XSource code : topologicalType}.
Hypothesis crsSource code : completely_regular_space X.

Let X'Source code : uniformType := @sup_topology X {fSource code : X -> R | continuous f}
  (fun fSource code => Uniform.class (initial_topology (projT1 f))).

Let completely_regular_nbhsESource code : @nbhs X X = nbhs_ (@entourage X').
Proof.
rewrite nbhs_entourageE; apply/funext => x; apply/seteqP; split; first last.
  apply/cvg_sup => -[f ctsf] U [/= _ [[V /= oV <- /= Vfx]]] /filterS.
  by apply; exact/ctsf/open_nbhs_nbhs.
move=> U; wlog oU : U / @open X U.
  move=> WH; rewrite nbhsE => -[V [oV Vx /filterS]].
  apply; first exact: (@nbhs_filter X').
  by apply: WH => //; move: oV; rewrite openE; exact.
move=> /[dup] nUx /nbhs_singleton Ux.
have ufs : uniform_separator [set x] (~` U).
  by apply: crs; [exact: open_closedC | exact].
have /uniform_separatorP := ufs => /(_ R)[f [ctsf f01 fx0 fU1]].
rewrite -nbhs_entourageE /entourage /= /sup_ent /= smallest_filter_finI.
pose E := map_pair f @^-1` (fun pqSource code => ball pq.1 1 pq.2).
exists E; first last.
  move=> z /= /set_mem; rewrite /E /=.
  have -> : f x = 0 by apply: fx0; exists x.
  rewrite /ball /= sub0r normrN; apply: contraPP => cUz.
  suff -> : f z = 1 by rewrite normr1 ltxx.
  by apply: fU1; exists z.
move=> r /= [_]; apply => /=.
pose f' : {classic {fSource code : X -> R | continuous f}} := exist _ f ctsf.
suff /asboolP entE : @entourage (initial_topology f) (f', E).2.
  by exists (exist _ (f', E) entE).
exists (fun pqSource code => ball pq.1 1 pq.2) => //=.
by rewrite /entourage /=; exists 1 => /=.
Qed.

Definition type

completely_regular_uniformity.type : realType -> forall {X : topologicalType}, completely_regular_space X -> Type completely_regular_uniformity.type is not universe polymorphic Arguments completely_regular_uniformity.type {R X} crs completely_regular_uniformity.type is transparent Expands to: Constant mathcomp.analysis.normedtype_theory.urysohn.completely_regular_uniformity.type Declared in library mathcomp.analysis.normedtype_theory.urysohn, line 476, characters 11-15

Source code : Type := let _ := completely_regular_nbhsE in X.

#[export]Source code HBSource code.instanceSource code DefinitionSource code _Source code :=Source code TopologicalSource code.copy type X.
#[export]Source code HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @Nbhs_isUniformSource code.Build
  type
  (@entourage X')
  (@entourage_filter X')
  (@entourage_diagonal_subproof X')
  (@entourage_inv X')
  (@entourage_split_ex X')
  completely_regular_nbhsE.

End completely_regular_uniformity.
Module ExportsSource code. HB.reexport. End Exports.
End completely_regular_uniformity.
Export completely_regular_uniformity.Exports.

Section locally_compact_uniform.
Context {XSource code : topologicalType} {RSource code : realType}.
Hypothesis lcptSource code : locally_compact [set: X].
Hypothesis hsdfSource code : hausdorff_space X.

Let opcSource code := @one_point_compactification X.

Lemma one_point_compactification_completely_regSource code :
  completely_regular_space opc.
Proof.
apply: (@normal_completely_regular R).
  apply: compact_normal.
    exact: one_point_compactification_hausdorff.
  exact: one_point_compactification_compact.
by apply: hausdorff_accessible; exact: one_point_compactification_hausdorff.
Qed.

#[local]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code UniformSource code.copy opc
  (@completely_regular_uniformity.type R _
    one_point_compactification_completely_reg).

Let X'Source code := @initial_topology X opc Some.
Lemma nbhs_one_point_compactification_weakESource code : @nbhs X X = nbhs_ (@entourage X').
Proof.
by rewrite nbhs_entourageE one_point_compactification_initial_topology.
Qed.

#[local,Source code non_forgetful_inheritance]Source code
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code @Nbhs_isUniformSource code.Build
  X
  (@entourage X')
  (@entourage_filter X')
  (@entourage_diagonal_subproof X')
  (@entourage_inv X')
  (@entourage_split_ex X')
  nbhs_one_point_compactification_weakE.

Lemma locally_compact_completely_regularSource code : completely_regular_space X.
Proof.
exact: uniform_completely_regular. Qed.

End locally_compact_uniform.

Lemma completely_regular_regularSource code {RSource code : realType} {XSource code : topologicalType} :
  completely_regular_space X -> @regular_space X.
Proof.
move=> crsX; pose P' := @completely_regular_uniformity.type R _ crsX.
exact: (@uniform_regular P').
Qed.

Section pseudometric_normal.

Lemma regular_openPSource code {TSource code : topologicalType} (xSource code : T) :
  {for x, @regular_space T} <-> forall ASource code, closed A -> ~ A x ->
  exists USource code VSource code : set T, [/\ open U, open V, U x, A `<=` V & U `&` V = set0].
Proof.
split.
  move=> + A clA nAx => /(_ (~` A)) [].
    by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
  move=> U Ux /subsetC; rewrite setCK => AclU; exists U°.
  exists (~` closure U) ; split => //; first exact: open_interior.
    exact/closed_openC/closed_closure.
  apply/disjoints_subset; rewrite setCK.
  exact: (subset_trans (@interior_subset _ _) (@subset_closure _ _)).
move=> + A Ax => /(_ (~` A°)) []; [|exact|].
  exact/open_closedC/open_interior.
move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U.
  exact/open_nbhs_nbhs.
apply: (subset_trans (closureS UV)).
move/open_closedC/closure_id : oV => <-.
by apply: (subset_trans cAV); rewrite setCK; exact: interior_subset.
Qed.

Lemma pseudometric_normalUsed by
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
Source code {RSource code : realType} {XSource code : pseudoMetricType R} :
  normal_space X.
Proof.
apply/(@normal_openP R) => A B clA clB AB0.
have eps' (DSource code : set X) : closed D -> forall xSource code, exists epsSource code : {posnum R}, ~ D x ->
    ball x eps%:num `&` D = set0.
  move=> clD x; have [nDx|?] := pselect (~ D x); last by exists 1%:pos.
  have /regular_openP/(_ _ clD) [//|] := @uniform_regular X x.
  move=> U [V] [+ oV] Ux /subsetC BV /disjoints_subset UV0.
  rewrite openE /interior => /(_ _ Ux); rewrite -nbhs_ballE => -[].
  move => _/posnumP[eps] beU; exists eps => _; apply/disjoints_subset.
  exact: (subset_trans beU (subset_trans UV0 _)).
pose epsA xSource code := projT1 (cid (eps' _ clB x)).
pose epsB xSource code := projT1 (cid (eps' _ clA x)).
exists (\bigcup_(xSource code in A) interior (ball x ((epsA x)%:num / 2)%:pos%:num)).
exists (\bigcup_(xSource code in B) interior (ball x ((epsB x)%:num / 2)%:pos%:num)).
split.
- by apply: bigcup_open => ? ?; exact: open_interior.
- by apply: bigcup_open => ? ?; exact: open_interior.
- by move=> x ?; exists x => //; exact: nbhsx_ballx.
- by move=> y ?; exists y => //; exact: nbhsx_ballx.
- apply/nonemptyPn => -[z [[x Ax /interior_subset Axe]]].
  case=> y By /interior_subset Bye; have nAy : ~ A y.
    by move: AB0; rewrite setIC => /disjoints_subset; exact.
  have nBx : ~ B x by move/disjoints_subset: AB0; exact.
  have [|/ltW] := leP ((epsA x)%:num / 2) ((epsB y)%:num / 2).
    move/ball_sym: Axe => /[swap] /le_ball /[apply] /(ball_triangle Bye).
    rewrite -splitr => byx; have := projT2 (cid (eps' _ clA y)) nAy.
    by rewrite -subset0; apply; split; [exact: byx|].
  move/ball_sym: Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe).
  rewrite -splitr => byx; have := projT2 (cid (eps' _ clB x)) nBx.
  by rewrite -subset0; apply; split; [exact: byx|].
Qed.

End pseudometric_normal.
Generated by rocqnavi
Source
Uses
Used By