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 { : uniformType} { : realType}.
Context ( : set T) ( : set (T * T)).
Hypothesis : entourage E.
Hypothesis : A `*` B `&` E = set0.

Local Notation := [the pseudoMetricType R of gauge.type entE].

Local Lemma : exists ( : T -> R),
[/\ continuous f, range f `<=` `[0, 1],
f @` A `<=` [set 0] & f @` B `<=` [set 1] ].

Proof.

have [eps exy] : exists ( : {posnum R}),
    forall ( : 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 => fine (@edist_inf R T' A z)) \min (fun=> eps%:num).
pose f := (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 { : topologicalType} { : realType}.

Definition ( : set T) :=
  exists ( : @Uniform.axioms_ T^o) ( : set (T * T)),
    let := Uniform.Pack uT in [/\
      @entourage UT E, A `*` B `&` E = set0 &
      (forall , @nbhs UT UT x `<=` @nbhs T T x)].

Local Lemma ( : set T) : exists ( : 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 ( : set T) : T -> R := projT1 (cid (Urysohn' A B)).

Section urysohn_facts.

Lemma ( : set T) : continuous (Urysohn A B).

Proof.

by have [] := projT2 (cid (@Urysohn' A B)). Qed.

Lemma ( : set T) : range (Urysohn A B) `<=` `[0, 1].

Proof.

by have [] := projT2 (cid (@Urysohn' A B)). Qed.

Lemma ( : 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 ( : 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 ( : 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 ( : 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 { : uniformType} ( : set T) :
(exists2 , 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 { : topologicalType}.
Hypothesis : normal_space T.
Section normal_uniform_separators.
Context ( : set T).

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

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

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

Local Lemma : 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 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 E ->
exists , [/\ ury_base E1, ury_base E2 &
(E1 `&` E2) \; (E1 `&` E2) `<=` E].

Proof.

case; case => L R [/= oL oR AL cLR <-].
have [R' []] : exists , [/\ 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 := smallest Filter ury_base.

Instance : Filter ury_unif.

Proof.

exact: smallest_filter_filter. Qed.

Local Lemma : ury_unif E -> diagonal `<=` E.

Proof.

by move/(_ (globally diagonal)); apply; split;
[exact: globally_filter|exact: ury_base_refl].
Qed.

Local Lemma : ury_unif E -> ury_unif E^-1.

Proof.

move=> ufE F [/filter_inv FF urF]; have [] := ufE [set V^-1 | 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 :
filterI_iter ury_base n E -> exists2 : 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 E ->
exists2 , 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 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 : Type := T.

..on urysohnType.

.
  isUniform.Build urysohnType ury_unif_filter ury_unif_refl ury_unif_inv
  ury_unif_split.
. T} := Pointed.copy urysohnType (Pointed.Pack p).

Lemma ( : 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 | 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 | _ \/ _].
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 { : topologicalType} { : realType} ( : set T) :
  uniform_separator A B <->
  exists ( : 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 | ball (f xy.1) 1 (f xy.2)]); split.
- exists [set | 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 { : realType} { : topologicalType}.

Let : [<->
normal_space T;
forall ( : set T), closed A -> closed B -> A `&` B = set0 ->
uniform_separator A B;
forall ( : set T), closed A -> closed B -> A `&` B = set0 ->
exists , [/\ 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_space T <->
forall ( : set T), closed A -> closed B -> A `&` B = set0 ->
exists , [/\ open U, open V, A `<=` U, B `<=` V & U `&` V = set0].

Proof.

exact: (normal_spaceP 0%N 2%N). Qed.

Lemma : normal_space T <->
forall ( : 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 { : 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 ( : topologicalType) :=
forall ( : T) ( : set T), closed B -> ~ B a -> uniform_separator [set a] B.

Lemma { : uniformType} ( : T) ( : 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 { : uniformType} :
@completely_regular_space T.

Proof.

by move=> x B clB Bx; exact: point_uniform_separator. Qed.

Lemma { : 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 { : 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 .
Section completely_regular_uniformity.
Context { : realType} { : topologicalType}.
Hypothesis : completely_regular_space X.

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

Let : @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 => 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 { : 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 => ball pq.1 1 pq.2) => //=.
by rewrite /entourage /=; exists 1 => /=.
Qed.

Definition : Type := let _ := completely_regular_nbhsE in X.

..copy type X.
..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 . HB.reexport. End Exports.
End completely_regular_uniformity.
Export completely_regular_uniformity.Exports.

Section locally_compact_uniform.
Context { : topologicalType} { : realType}.
Hypothesis : locally_compact [set: X].
Hypothesis : hausdorff_space X.

Let := @one_point_compactification X.

Lemma :
  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.

..copy opc
(@completely_regular_uniformity.type R _
one_point_compactification_completely_reg).

Let := @initial_topology X opc Some.
Lemma : @nbhs X X = nbhs_ (@entourage X').

Proof.

by rewrite nbhs_entourageE one_point_compactification_initial_topology.
Qed.

..Build
  X
  (@entourage X')
  (@entourage_filter X')
  (@entourage_diagonal_subproof X')
  (@entourage_inv X')
  (@entourage_split_ex X')
  nbhs_one_point_compactification_weakE.

Lemma : completely_regular_space X.

Proof.

exact: uniform_completely_regular. Qed.

End locally_compact_uniform.

Lemma { : realType} { : 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 { : topologicalType} ( : T) :
{for x, @regular_space T} <-> forall , closed A -> ~ A x ->
exists : 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 { : realType} { : pseudoMetricType R} :
normal_space X.

Proof.

apply/(@normal_openP R) => A B clA clB AB0.
have eps' ( : set X) : closed D -> forall , exists : {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 := projT1 (cid (eps' _ clB x)).
pose epsB := projT1 (cid (eps' _ clA x)).
exists (\bigcup_( in A) interior (ball x ((epsA x)%:num / 2)%:pos%:num)).
exists (\bigcup_( 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.

Files

Module mathcomp.analysis.normedtype_theory.urysohn