Module mathcomp.analysis.topology_theory.num_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
From mathcomp Require Import interval_inference reals topology_structure.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import uniform_structure pseudometric_structure.
From mathcomp Require Import order_topology matrix_topology.


Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+").
Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-").

Import Order.TTheory GRing.Theory Num.Theory.

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numDomainTypeSource code

) := hasNbhs.Build R^o
  (nbhs_ball_ (ball_ (fun

xSource code

=> `|x|))).

Module

TopologicalNumDomainTypeSource code

.
Section TopologicalNumDomainType.
Context {

RSource code

: numDomainType}.

Lemma

nbhs_filterSource code

 (

pSource code

: R^o) : ProperFilter (nbhs p).

Proof.

split.
  by move=> [] e e0 /subsetP/(_ p); rewrite !in_setE/= subrr normr0.
split=> [|P Q|P Q].
- by exists 1; [exact: ltr01|exact: subsetT].
- move=> [] /= e e0 /subsetP eP [] /= f f0 /subsetP fQ.
  exists (Order.min e f) => /=.
    by rewrite [Num.min e f]/(Order.min e f); case: ifP.
  apply/subsetP => x.
  rewrite in_setE in_setI/= => pef.
  apply/andP; split.
    apply/eP/mem_set/(lt_le_trans pef).
    by case: (@real_ltP _ e f) => //; exact: gtr0_real.
  apply/fQ/mem_set/(lt_le_trans pef).
  by case: (@real_ltP _ f e) => //; exact: gtr0_real.
- move=> PQ [] /= e e0 eP.
  by exists e => //; exact: (subset_trans eP).
Qed.

Lemma

nbhs_singletonSource code

 (

pSource code

: R^o) (

ASource code

: set R) : nbhs p A -> A p.

Proof.

move=> [] /= e e0 /subsetP /(_ p).
by rewrite !in_setE/= subrr normr0 e0 => /(_ erefl).
Qed.

Lemma

nbhs_nbhsSource code

 (

pSource code

: R^o) (

ASource code

: set R) : nbhs p A -> nbhs p (nbhs^~ A).

Proof.

move=> [] /= e e0 /subsetP eA; exists e => //.
apply/subsetP => x /[!inE]/= xe.
exists (e - `|p - x|); first by rewrite /= subr_gt0.
apply/subsetP => y; rewrite inE/= ltrBrDl => ye.
apply/eA/mem_set => /=.
by rewrite -(subrK x p) -addrA (le_lt_trans (ler_normD _ _)).
Qed.

End TopologicalNumDomainType.

End TopologicalNumDomainType.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numDomainTypeSource code

) := Nbhs_isNbhsTopological.Build R^o
  (@TopologicalNumDomainType.nbhs_filter R)
  (@TopologicalNumDomainType.nbhs_singleton R)
  (@TopologicalNumDomainType.nbhs_nbhs R).

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numFieldTypeSource code

) := Nbhs_isPseudoMetric.Build R R^o
  nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numFieldTypeSource code

) :=
  Uniform_isPseudoMetric.Build R R^o
    ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.

Lemma

real_order_nbhsESource code

 (

RSource code

: realFieldType) (

xSource code

: R^o) : nbhs x =
  filter_from (fun

iSource code

=> itv_open_ends i /\ x \in i) (fun

iSource code

=> [set` i]).

Proof.

rewrite eqEsubset; split => U.
  case => _ /posnumP[e] xeU.
  exists (`]x - e%:num, x + e%:num[); first split => //.
    by rewrite in_itv/= -lter_distl subrr normr0.
  apply: subset_trans xeU => z /=.
  by rewrite in_itv /= -lter_distl distrC.
case => [][[[]l|[]]] [[]r|[]] []//= _.
- move=> xlr lrU; exists (Order.min (x - l) (r - x)).
    by rewrite /= lt_min ?lterBDr ?add0r ?(itvP xlr).
  apply/(subset_trans _ lrU)/subset_ball_prop_in_itv.
  suff : (`]x - Order.min (x - l) (r - x), x + Order.min (x - l) (r - x)[
          <= `]l, r[)%O by move/subitvP => H ? ?; exact: H.
  rewrite subitvE 2!lteBSide/=.
  by rewrite lerBrDl [_ + l]addrC -2!lerBrDl 2!ge_min 2!lexx orbT.
- move=> xl lU; exists (x - l) => /=; first by rewrite lterBDr add0r (itvP xl).
  apply/(subset_trans _ lU)/subset_ball_prop_in_itv.
  suff : (`]x - (x - l), x + (x - l)[ <= `]l, +oo[)%O.
    by move/subitvP => + ?; exact.
  by rewrite subitvE lteBSide/= subKr lexx.
- move=> xr rU; exists (r - x) => /=; first by rewrite lterBDr add0r (itvP xr).
  apply/(subset_trans _ rU)/subset_ball_prop_in_itv.
  suff : (`]x - (r - x), x + (r - x)[ <= `]-oo, r[)%O.
    by move/subitvP => + ?; exact.
  by rewrite subitvE lteBSide/= addrC subrK.
- by move=> _; rewrite set_itvE subTset => ->; exists 1 => /=.
Qed.

Module

numFieldTopologySource code

.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

realTypeSource code

) := PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

rcfTypeSource code

) := PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

archiRealFieldTypeSource code

) := PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

realFieldTypeSource code

) := PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numClosedFieldTypeSource code

) :=
  PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

numFieldTypeSource code

) := PseudoPointedMetric.copy R R^o.

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

realFieldTypeSource code

) :=
  Order_isNbhs.Build _ R (@real_order_nbhsE R).

#[export,Source code

non_forgetful_inheritance]Source code

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

 (

RSource code

:Source code

realTypeSource code

) :=
  Order_isNbhs.Build _ R (@real_order_nbhsE R).

Module

ExportsUsed by

• mathcomp.analysis.topology_theory.separation_axioms
• mathcomp.analysis.normedtype_theory.normed_module

---

Source code

. HB.reexport. End Exports.

End numFieldTopology.
Import numFieldTopology.Exports.

Lemma

nbhsNSource code

{

RSource code

: numFieldType} (

xSource code

: R) : nbhs (- x) = -%R @ x.

Proof.

rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=.
  by move=> ?; apply: xeA => //=; rewrite -opprD normrN.
by rewrite -opprD normrN => ?; rewrite -[y]opprK; apply: xeA; rewrite /= opprK.
Qed.

Lemma

cvg_compNPUsed by

• mathcomp.analysis.ftc

---

Source code

{

TSource code

: topologicalType} {

RSource code

: numFieldType} (

fSource code

: R -> T) (

aSource code

: R)
    (

lSource code

: T) :
  (f \o -%R) x @[

xSource code

--> a] --> l <-> f x @[

xSource code

--> (- a)] --> l.

Proof.

by rewrite nbhsN. Qed.

Lemma

withinNUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

{

RSource code

: numFieldType} (

ASource code

: set R) (

rSource code

: R) :
  within A (nbhs (- r)) = - x @[

xSource code

--> within (-%R @` A) (nbhs r)].

Proof.

rewrite eqEsubset /=; split; move=> E /= [e e0 reE]; exists e => //.
  move=> s rse sA; apply: reE; last by rewrite memNE opprK.
  by rewrite /= opprK addrC distrC.
move=> s res rs; rewrite -(opprK s); apply: reE; last by rewrite -memNE.
by rewrite /= opprK -normrN opprD.
Qed.

Lemma

nearNUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

{

RSource code

: numFieldType} (

xSource code

: R) (

PSource code

: R -> Prop) :
  (\forall

ySource code

\near - x, P y) <-> \near

xSource code

, P (- x).

Proof.

by rewrite -[X in X <-> _]near_simpl nbhsN. Qed.

Lemma

nbhsNimageSource code

{

RSource code

: numFieldType} (

xSource code

: R) :
  nbhs (- x) = [set -%R @` A |

ASource code

in nbhs x].

Proof.

rewrite nbhsN /fmap/=; under eq_set => A do rewrite preimageEinv//= inv_oppr.
by rewrite (eq_imageK opprK opprK).
Qed.

Lemma

openNSource code

{

RSource code

: numFieldType} (

ASource code

: set R) : open A -> open [set - x |

xSource code

in A].

Proof.

move=> Aop; rewrite openE => _ [x /Aop x_A <-].
by rewrite /interior nbhsNimage; exists A.
Qed.

Lemma

closedNSource code

 (

RSource code

: numFieldType) (

ASource code

: set R) :
  closed A -> closed [set - x |

xSource code

in A].

Proof.

move=> Acl x clNAx.
suff /Acl : closure A (- x) by exists (- x)=> //; rewrite opprK.
move=> B oppx_B; have : [set - x |

xSource code

in A] `&` [set - x |

xSource code

in B] !=set0.
  by apply: clNAx; rewrite -[x]opprK nbhsNimage; exists B.
move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
Qed.

Lemma

dnbhsNUsed by

• mathcomp.analysis.normedtype_theory.normed_module

---

Source code

{

RSource code

: numFieldType} (

rSource code

: R) :
  (- r)%R^' = (fun

ASource code

=> -%R @` A) @` r^'.

Proof.

apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
  exists (-%R @` A).
    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
  by rewrite opprK.
exists e => //= x/=; rewrite -opprD normrN => axe xa.
exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
by rewrite opprK.
Qed.

Section at_left_right.
Context {

RSource code

: numFieldType}.

Definition

at_left

---

Used by

• mathcomp.analysis.derive
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

 (

xSource code

: R) := within (fun

uSource code

=> u < x) (nbhs x).
Definition

at_right

---

Used by

• mathcomp.analysis.derive
• mathcomp.analysis.lebesgue_stieltjes_measure
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

 (

xSource code

: R) := within (fun

uSource code

=> x < u) (nbhs x).
Local Notation 

"x ^'-"Source code

:= (at_left x) : classical_set_scope.
Local Notation 

"x ^'+"Source code

:= (at_right x) : classical_set_scope.

Global Instance

at_right_proper_filterUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule
• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

 (

xSource code

: R) : ProperFilter x^'+.

Proof.

apply: Build_ProperFilter => -[_/posnumP[d] /(_ (x + d%:num / 2))].
apply; last by rewrite ltrDl.
by rewrite /= opprD addNKr normrN ger0_norm// gtr_pMr// invf_lt1// ltr1n.
Qed.

Global Instance

at_left_proper_filterUsed by

• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule
• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

 (

xSource code

: R) : ProperFilter x^'-.

Proof.

apply: Build_ProperFilter => -[_ /posnumP[d] /(_ (x - d%:num / 2))].
apply; last by rewrite gtrBl.
by rewrite /= opprB addrC subrK ger0_norm// gtr_pMr// invf_lt1// ltr1n.
Qed.

Lemma

cvg_dnbhs_at_rightUsed by

• mathcomp.analysis.realfun

---

Source code

 (

TSource code

: topologicalType) (

fSource code

: R -> T) (

pSource code

: R) (

lSource code

: T) :
  f x @[

xSource code

--> p^'] --> l -> f x @[

xSource code

--> p^'+] --> l.

Proof.

by apply: cvg_trans; apply: cvg_app; apply: within_subset=> r ?; rewrite gt_eqF.
Qed.

Lemma

cvg_dnbhs_at_leftUsed by

• mathcomp.analysis.realfun

---

Source code

 (

TSource code

: topologicalType) (

fSource code

: R -> T) (

pSource code

: R) (

lSource code

: T) :
  f x @[

xSource code

--> p^'] --> l -> f x @[

xSource code

--> p^'-] --> l.

Proof.

by apply: cvg_trans; apply: cvg_app; apply: within_subset=> r ?; rewrite lt_eqF.
Qed.

Lemma

nbhs_right_gtUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.topology_theory.metric_structure
• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'+, x < y.

Proof.

by rewrite near_withinE; apply: nearW. Qed.

Lemma

nbhs_left_ltUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'-, y < x.

Proof.

by rewrite near_withinE; apply: nearW. Qed.

Lemma

nbhs_right_neqUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'+, y != x.

Proof.

by rewrite near_withinE; apply: nearW => ? /gt_eqF->. Qed.

Lemma

nbhs_left_neqUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'-, y != x.

Proof.

by rewrite near_withinE; apply: nearW => ? /lt_eqF->. Qed.

Lemma

nbhs_right_geUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'+, x <= y.

Proof.

by rewrite near_withinE; apply: nearW; apply/ltW. Qed.

Lemma

nbhs_left_leUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

: \forall

ySource code

\near x^'-, y <= x.

Proof.

by rewrite near_withinE; apply: nearW => ?; apply/ltW. Qed.

Lemma

nbhs_right_ltUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.topology_theory.metric_structure
• mathcomp.analysis.realfun
• mathcomp.analysis.normedtype_theory.normed_module
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

zSource code

: x < z -> \forall

ySource code

\near x^'+, y < z.

Proof.

move=> xz; exists (z - x) => //=; first by rewrite subr_gt0.
by move=> y /= + xy; rewrite distrC ?ger0_norm ?subr_ge0 1?ltW// ltrD2r.
Qed.

Lemma

nbhs_right_ltWUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.ftc

---

Source code

xSource code

zSource code

: x < z -> \forall

ySource code

\near nbhs x^'+, y <= z.

Proof.

by move=> xz; near=> y; apply/ltW; near: y; exact: nbhs_right_lt.
Unshelve. all: by end_near. Qed.

Lemma

nbhs_right_ltDrUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc

---

Source code

xSource code

eSource code

: 0 < e -> \forall

ySource code

\near x ^'+, y - x < e.

Proof.

move=> e0; near=> y; rewrite ltrBlDr; near: y.
by apply: nbhs_right_lt; rewrite ltrDr.
Unshelve. all: by end_near. Qed.

Lemma

nbhs_right_leUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.exp
• mathcomp.analysis.topology_theory.metric_structure
• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.normed_module
• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

xSource code

zSource code

: x < z -> \forall

ySource code

\near x^'+, y <= z.

Proof.

by move=> xz; near do apply/ltW; apply: nbhs_right_lt.
Unshelve. all: by end_near. Qed.

Lemma

not_near_at_rightPUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

 (

pSource code

: R) (

PSource code

: pred R) :
  ~ (\forall

xSource code

\near p^'+, P x) <->
  forall

eSource code

: {posnum R}, exists2

xSource code

, p < x < p + e%:num & ~ P x.

Proof.

split=> [pPf e|ex_notPx].
- apply: contrapT => /forallPNP peP; apply: pPf; near=> t.
  apply: contrapT; apply: peP; apply/andP; split.
  + by near: t; exact: nbhs_right_gt.
  + by near: t; apply: nbhs_right_lt; rewrite ltrDl.
- rewrite /at_right near_withinE nearE.
  rewrite -filter_from_ballE /filter_from/= -forallPNP => _ /posnumP[d].
  have [x /andP[px xpd] notPx] := ex_notPx d; rewrite -existsNP; exists x => /=.
  apply: contra_not notPx; apply => //.
  by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
Unshelve. all: by end_near. Qed.

Lemma

at_rightDSource code

xSource code

aSource code

: (x + a)^'+ = (y + a @[

ySource code

--> x^'+]).

Proof.

apply/seteqP; split=> A /=.
- move=> [/= r r0 xarA]; exists r => // y bxy x_lt_y.
  by apply: xarA => /=; rewrite ?ltrD2r// (addrC y) addrKA.
- move=> [/= r r0 xrAa]; exists r => // y bxay xay.
  by rewrite -(subrK a y); apply: xrAa => /=; rewrite ?ltrBrDr// opprB addrA.
Qed.

Lemma

at_leftDSource code

xSource code

aSource code

: (x + a)^'- = (y + a @[

ySource code

--> x^'-]).

Proof.

apply/seteqP; split=> A /=.
- move=> [/= r r0 xarA]; exists r => // y bxy x_lt_y.
  by apply: xarA => /=; rewrite ?ltrD2r// (addrC y) addrKA.
- move=> [/= r r0 xrAa]; exists r => // y bxay yxa.
  by rewrite -(subrK a y); apply: xrAa => /=; rewrite ?ltrBlDr// opprB addrA.
Qed.

Lemma

near_at_rightDSource code

xSource code

aSource code

 (

PSource code

: set R) :
  (\forall

ySource code

\near (x + a)^'+, P y) = (\forall

ySource code

\near x^'+, P (y + a)).

Proof.

by rewrite at_rightD near_map. Qed.

Lemma

near_at_leftDSource code

xSource code

aSource code

 (

PSource code

: set R) :
  (\forall

ySource code

\near (x + a)^'-, P y) = (\forall

ySource code

\near x^'-, P (y + a)).

Proof.

by rewrite at_leftD near_map. Qed.

Lemma

at_left_shiftSource code

 (

TSource code

: Type)

xSource code

aSource code

 (

fSource code

: R -> T) :
  (f @ (x + a)^'-) = (f (y + a) @[

ySource code

--> x^'-]).

Proof.

by rewrite at_leftD. Qed.

Lemma

at_right_shiftUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

 (

TSource code

: Type)

xSource code

aSource code

 (

fSource code

: R -> T) :
  (f @ (x + a)^'+) = (f (y + a) @[

ySource code

--> x^'+]).

Proof.

by rewrite at_rightD. Qed.

Context {

VSource code

: topologicalType} (

fSource code

: R -> V) (

xSource code

: R).

Lemma

cvg_at_right_filterUsed by

• mathcomp.analysis.pi_irrational
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation
• mathcomp.analysis.exp
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.probability_theory.beta_distribution
• mathcomp.analysis.probability_theory.exponential_distribution
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.elementary_functions.trigonometry_integral

---

Source code

 (

lSource code

: V) :
  f z @[

zSource code

--> x] --> l -> f z @[

zSource code

--> x^'+] --> l.

Proof.

exact: (@cvg_within_filter _ _ _ (nbhs x)). Qed.

Lemma

cvg_at_left_filterUsed by

• mathcomp.analysis.pi_irrational
• mathcomp.analysis.exp
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.probability_theory.beta_distribution
• mathcomp.analysis.probability_theory.exponential_distribution
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.elementary_functions.trigonometry_integral

---

Source code

 (

lSource code

: V) :
  f z @[

zSource code

--> x] --> l -> f z @[

zSource code

--> x^'-] --> l.

Proof.

exact: (@cvg_within_filter _ _ _ (nbhs x)). Qed.

Lemma

cvg_at_right_withinUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

: f x @[

xSource code

--> x^'+] --> f x ->
  f x @[

xSource code

--> within (fun

uSource code

=> x <= u) (nbhs x)] --> f x.

Proof.

move=> fxr U Ux; rewrite ?near_simpl ?near_withinE; near=> z; rewrite le_eqVlt.
by move/predU1P => [<-|]; [exact: nbhs_singleton | near: z; exact: fxr].
Unshelve. all: by end_near. Qed.

Lemma

cvg_at_left_withinUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

: f x @[

xSource code

--> x^'-] --> f x ->
  f x @[

xSource code

--> within (fun

uSource code

=> u <= x) (nbhs x)] --> f x.

Proof.

move=> fxr U Ux; rewrite ?near_simpl ?near_withinE; near=> z; rewrite le_eqVlt.
by move/predU1P => [->|]; [exact: nbhs_singleton | near: z; exact: fxr].
Unshelve. all: by end_near. Qed.

End at_left_right.
#[global] Typeclasses Opaque at_left at_right.
Notation 

"x ^'-"Source code

:= (at_left x) : classical_set_scope.
Notation 

"x ^'+"Source code

:= (at_right x) : classical_set_scope.

#[global] Hint Extern 0 (Filter (nbhs _^'+)) =>
  (apply: at_right_proper_filter) : typeclass_instances.

#[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
  (apply: at_left_proper_filter) : typeclass_instances.

Lemma

cvg_at_right_left_dnbhsUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc

---

Source code

 (

RSource code

: realFieldType) (

TSource code

: topologicalType)
    (

fSource code

: R -> T) (

pSource code

: R) (

lSource code

: T) :
  f x @[

xSource code

--> p^'+] --> l -> f x @[

xSource code

--> p^'-] --> l -> f x @[

xSource code

--> p^'] --> l.

Proof.

move=> + + U Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
rewrite !near_withinE !near_nbhs => lf rf.
apply: filter_app lf; apply: filter_app rf.
by near=> t => xlt xgt /lt_total/orP[|].
Unshelve. all: by end_near. Qed.

Lemma

left_right_continuousPUsed by

• mathcomp.analysis.realfun
• mathcomp.analysis.ftc

---

Source code

{

RSource code

: realFieldType} {

TSource code

: topologicalType}
    (

fSource code

: R -> T)

xSource code

:
  f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x.

Proof.

split; last by move=> cts; split; exact: cvg_within_filter.
move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl.
rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf.
near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real.
move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//].
- by move=> <-; exact: nbhs_singleton.
- by move=> ->; exact: nbhs_singleton.
Unshelve. all: by end_near. Qed.

Lemma

closure_supUsed by

• mathcomp.analysis.normedtype_theory.normed_module

---

Source code

 (

RSource code

: realType) (

ASource code

: set R) :
  A !=set0 -> has_ubound A -> closure A (sup A).

Proof.

move=> A0 ?; have [|AsupA] := pselect (A (sup A)); first exact: subset_closure.
rewrite closure_isolated_limit_point.
right => U /nbhs_ballP[_ /posnumP[e]] supAeU.
suff [x [Ax /andP[sAex xsA]]] : exists

xSource code

, A x /\ sup A - e%:num < x < sup A.
  exists x; split => //; first by rewrite lt_eqF.
  apply supAeU; rewrite /ball /= ltr_distl (addrC x e%:num) -ltrBlDl sAex.
  by rewrite andbT (le_lt_trans _ xsA) // lerBlDl lerDr.
apply: contrapT => /forallNP Ax.
suff /(ge_sup A0) : ubound A (sup A - e%:num).
  by rewrite leNgt => /negP; apply; rewrite ltrBlDl ltrDr.
move=> y Ay; have /not_andP[//|/negP] := Ax y.
rewrite negb_and leNgt => /orP[//|]; apply: contra => sAey.
rewrite lt_neqAle sup_upper_bound // andbT.
by apply: contra_not_neq AsupA => <-.
Qed.

Lemma

right_bounded_interiorUsed by

• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

 (

RSource code

: realType) (

XSource code

: set R) :
  has_ubound X -> X° `<=` [set

rSource code

| r < sup X].

Proof.

move=> uX r Xr; rewrite /mkset ltNge; apply/negP.
rewrite le_eqVlt => /orP[/eqP supXr|]; last first.
  by apply/negP; rewrite -leNgt ub_le_sup//; exact: interior_subset.
suff : ~ X° (sup X) by rewrite supXr.
case/nbhs_ballP => _/posnumP[e] supXeX.
have [f XsupXf] : exists

fSource code

: {posnum R}, X (sup X + f%:num).
  exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprD addNKr normrN.
  by rewrite gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n.
have : sup X + f%:num <= sup X by exact: ub_le_sup.
by apply/negP; rewrite -ltNge; rewrite ltrDl.
Qed.

Lemma

left_bounded_interiorUsed by

• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

 (

RSource code

: realType) (

XSource code

: set R) :
  has_lbound X -> X° `<=` [set

rSource code

| inf X < r].

Proof.

move=> lX r Xr; rewrite /mkset ltNge; apply/negP.
rewrite le_eqVlt => /orP[/eqP rinfX|]; last first.
  by apply/negP; rewrite -leNgt ge_inf//; exact: interior_subset.
suff : ~ X° (inf X) by rewrite -rinfX.
case/nbhs_ballP => _/posnumP[e] supXeX.
have [f XsupXf] : exists

fSource code

: {posnum R}, X (inf X - f%:num).
  exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprB addrC subrK.
  by rewrite gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n.
have : inf X <= inf X - f%:num by exact: ge_inf.
by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl.
Qed.

Lemma

in_continuous_mksetPUsed by

• mathcomp.analysis.ftc
• mathcomp.analysis.normedtype_theory.num_normedtype

---

Source code

{

TSource code

: realFieldType} {

USource code

: nbhsType}
    (

iSource code

: interval T) (

fSource code

: T -> U) :
  {in i, continuous f} <-> {in [set` i], continuous f}.

Proof.

by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE].
Qed.

Lemma

nbhs0_ltWUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation

---

Source code

 (

RSource code

: realFieldType) (

xSource code

: R) : (0 < x)%R ->
 \forall

rSource code

\near nbhs (0%R:R), (r <= x)%R.

Proof.

exists x => // y; rewrite /ball/= sub0r normrN => /ltW.
by apply: le_trans; rewrite ler_norm.
Qed.

Lemma

nbhs0_ltSource code

 (

RSource code

: realFieldType) (

xSource code

: R) : (0 < x)%R ->
 \forall

rSource code

\near nbhs (0%R:R), (r < x)%R.

Proof.

exists x => // z /=; rewrite sub0r normrN.
by apply: le_lt_trans; rewrite ler_norm.
Qed.

Lemma

lt_nbhslUsed by

• mathcomp.analysis.probability_theory.normal_distribution

---

Source code

{

RSource code

: realFieldType} (

xSource code

aSource code

: R) : x < a ->
  \forall

ySource code

\near nbhs x, y < a.

Proof.

move=> xb; exists ((a - x) / 2) => /=; first by rewrite divr_gt0// subr_gt0.
move=> r/=; rewrite ltr_pdivlMr// ltrBrDr; apply: le_lt_trans.
by rewrite -lerBlDr -normrN opprB (le_trans (ler_norm _))// ler_peMr// ler1n.
Qed.

Lemma

lt_le_nbhslSource code

{

RSource code

: realFieldType} (

tSource code

xSource code

: R) :
  x < t -> \forall

ySource code

\near nbhs x, y <= t.

Proof.

by move/lt_nbhsl; apply: filterS => y /ltW. Qed.

Lemma

Nlt_nbhslUsed by

• mathcomp.analysis.ftc

---

Source code

{

RSource code

: realType} (

xSource code

aSource code

: R) :
  - x < a -> \forall

ySource code

\near nbhs x, - y < a.

Proof.

move=> xb; exists ((a + x) / 2) => /=.
  by rewrite divr_gt0// -(opprK x) subr_gt0.
move=> r/=; rewrite ltr_pdivlMr// -ltrBlDr; apply: le_lt_trans.
by rewrite -lerBlDr opprK addrC (le_trans (ler_norm _))// ler_peMr// ler1n.
Qed.

Lemma

near_right_in_itvUsed by

• mathcomp.analysis.realfun

---

Source code

{

RSource code

: realFieldType} (

aSource code

: R) (

PSource code

: set R) :
  (\forall

bSource code

\near a^'+, {in `]a, b[, forall

xSource code

, P x})
  <-> {near a^'+, forall

xSource code

, P x}.

Proof.

split=> [[/= _/posnumP[r] arP]|[/= r r0 arP]].
- exists (r%:num / 2) => [//=|x /= /ltr_distlCDr xar2 ax].
  apply: (arP (a + r%:num / 2)) => /=.
  + by rewrite opprD addNKr normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n.
  + by rewrite ltrDl.
  + by rewrite in_itv/= ax.
- exists r => // x /= /ltr_distlCDr xar ax y /[!in_itv]/= /andP[ay yx].
  apply: arP => //=.
  by rewrite distrC gtr0_norm ?subr_gt0// ltrBlDl (lt_trans _ xar).
Qed.

Lemma

near_left_in_itvSource code

{

RSource code

: realFieldType} (

bSource code

: R) (

PSource code

: set R) :
  (\forall

aSource code

\near b^'-, {in `]a, b[, forall

xSource code

, P x})
  <-> {near b^'-, forall

xSource code

, P x}.

Proof.

split=> [[/= _/posnumP[r] brP]|[/= r r0 brP]].
- exists (r%:num / 2) => [//=|x /= /ltr_distlDr bxr xb].
  apply: (brP (b - r%:num / 2)) => /=.
  + rewrite subKr gtr0_norm ?divr_gt0//.
    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
  + by rewrite gtrBl divr_gt0.
  + by rewrite in_itv/= xb andbT ltrBlDr.
- exists r => // x /= /ltr_distlDr bxr xb y /[!in_itv]/= /andP[xy yb].
  apply: brP => //=.
  by rewrite gtr0_norm ?subr_gt0// ltrBlDl (lt_trans bxr)// ltrD2r.
Qed.

Section nbhs_lt_le.
Context {

RSource code

: numFieldType}.
Implicit Types x z : R.

Lemma

lt_nbhsl_ltSource code

xSource code

zSource code

: x < z -> \forall

ySource code

\near x, x <= y -> y < z.

Proof.

move=> xz; near=> y.
rewrite le_eqVlt => /predU1P[<-//|].
near: y; exists (z - x) => /=; first by rewrite subr_gt0.
move=> y/= /[swap] xy; rewrite ltr0_norm ?subr_lt0//.
by rewrite opprD addrC ltrBlDr subrK opprK.
Unshelve. all: by end_near. Qed.

Lemma

lt_nbhsl_leUsed by

• mathcomp.analysis.ftc

---

Source code

xSource code

zSource code

: x < z -> \forall

ySource code

\near x, x <= y -> y <= z.

Proof.

by move=> xz; apply: filterS (lt_nbhsl_lt xz) => y /[apply] /ltW.
Qed.

End nbhs_lt_le.

Lemma

lt_nbhsrUsed by

• mathcomp.analysis.exp
• mathcomp.analysis.probability_theory.normal_distribution
• mathcomp.analysis.probability_theory.exponential_distribution
• mathcomp.analysis.realfun

---

Source code

{

RSource code

: realFieldType} (

aSource code

zSource code

: R) : a < z ->
  \forall

xSource code

\near z, a < x.

Proof.

rewrite -subr_gt0 => za0; exists (z - a) => //= u/=.
rewrite ltrBrDl addrC -ltrBrDl => /lt_le_trans; apply.
rewrite lerBlDl.
have [uz|uz] := leP u z.
  by rewrite ger0_norm ?subr_ge0// subrK.
by rewrite ltr0_norm ?subr_lt0// opprB addrAC -lerBlDr opprK lerD// ?ltW.
Qed.

Lemma

lt_le_nbhsrSource code

{

RSource code

: realFieldType} (

tSource code

xSource code

: R) :
  t < x -> \forall

ySource code

\near nbhs x, t <= y.

Proof.

by move/lt_nbhsr; apply: filterS => y /ltW. Qed.

Lemma

not_nearPSource code

{

TSource code

: topologicalType} (

pSource code

: T) (

PSource code

: set T) :
  ~ (\forall

xSource code

\near p, P x) <->
  forall

VSource code

: set T, nbhs p V -> exists2

xSource code

, V x & ~ P x.

Proof.

split.
- by contra => -[V + hV]; exact: filterS.
- by move=> /(_ P) /[apply] => -[].
Unshelve. all: by end_near. Qed.

Lemma

not_nearPballSource code

{

RSource code

: numDomainType} {

MSource code

: pseudoMetricType R}
    (

pSource code

: M) (

PSource code

: set M) :
  ~ (\forall

xSource code

\near p, P x) <->
  forall (

eSource code

: {posnum R}), exists2

xSource code

, ball p e%:num x & ~ P x.

Proof.

rewrite not_nearP; split.
- by move=> + e; apply; exact: nbhsx_ballx.
- rewrite -nbhs_ballE => + V [/= e e0 beV].
  by move=> /(_ (PosNum e0))[x /beV ? ?]; exists x.
Qed.

Global Instance

Proper_dnbhs_regular_numFieldTypeSource code

 (

RSource code

: numFieldType) (

xSource code

: R^o) :
  ProperFilter x^'.

Proof.

apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae].
exists (x + e%:num / 2)%R; apply: Ae; last by rewrite addrC -subr_eq0 addrK.
by rewrite /ball /= opprD addNKr normrN ger0_norm// [ltRHS]splitr ltr_pwDl.
Qed.

Global Instance

Proper_dnbhs_numFieldTypeUsed by

• mathcomp.analysis.ereal

---

Source code

 (

RSource code

: numFieldType) (

xSource code

: R) :
  ProperFilter x^'.

Proof.

apply: Build_ProperFilter_ex => A /nbhs_ballP[_/posnumP[e] Ae].
exists (x + e%:num / 2)%R; apply: Ae; last by rewrite addrC -subr_eq0 addrK.
by rewrite /ball /= opprD addNKr normrN ger0_norm// [ltRHS]splitr ltr_pwDl.
Qed.

Lemma

dense_ratUsed by

• mathcomp.analysis.borel_hierarchy
• mathcomp.analysis.normedtype_theory.normed_module

---

Source code

 (

RSource code

: realType) : dense (@ratr R @` setT).

Proof.

move=> A [r Ar]; rewrite openE => /(_ _ Ar)/nbhs_ballP[_/posnumP[e] reA].
have /rat_in_itvoo[q /itvP qre] : r < r + e%:num by rewrite ltrDl.
exists (ratr q) => //; split; last by exists q.
apply: reA; rewrite /ball /= distrC ltr_distl qre andbT.
by rewrite (@le_lt_trans _ _ r)// ?qre// lerBlDl lerDr ltW.
Qed.

Lemma

separated_open_countableUsed by

• mathcomp.analysis.normedtype_theory.vitali_lemma

---

Source code

    {

RSource code

: realType} (

ISource code

: Type) (

BSource code

: I -> set R) (

DSource code

: set I) :
    (forall

iSource code

, open (B i)) -> (forall

iSource code

, B i !=set0) ->
  trivIset D B -> countable D.

Proof.

move=> oB B0 tB; have [f fB] :
    {

fSource code

: I -> rat & forall

iSource code

, D i -> B i (ratr (f i))}.
  apply: (@choice _ _ (fun

xSource code

ySource code

=> D x -> B x (ratr y))) => i.
  have [r [Bir [q _ qr]]] := dense_rat (B0 _) (oB i).
  by exists q => Di; rewrite qr.
have inj_f : {in D &, injective f}.
  move=> i j /[!inE] Di Dj /(congr1 ratr) ratrij.
  have ? : (B i `&` B j) (ratr (f i)).
    by split => //; [exact: fB|rewrite ratrij; exact: fB].
  by apply/(tB _ _ Di Dj); exists (ratr (f i)).
apply/pcard_injP; have /card_bijP/cid[g bijg] := card_rat.
pose nat_of_rat (

qSource code

: rat) : nat := set_val (g (to_setT q)).
have inj_nat_of_rat : injective nat_of_rat.
  rewrite /nat_of_rat; apply: inj_comp => //; apply: inj_comp => //.
  exact/bij_inj.
by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact.
Qed.

Lemma

continuous_rsubmxUsed by

• mathcomp.analysis.derive

---

Source code

{

RSource code

: numFieldType}

mSource code

{

n1Source code

n2Source code

} :
  continuous (rsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n2)).

Proof.

move=> u A /nbhs_ballP[e /= e0 eA].
apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j.
by apply: (le_lt_trans _ (uv i (rshift n1 j))); rewrite !mxE.
Qed.

Lemma

continuous_lsubmxUsed by

• mathcomp.analysis.derive

---

Source code

{

RSource code

: numFieldType}

mSource code

{

n1Source code

n2Source code

} :
  continuous (lsubmx : 'M[R]_(m, n1 + n2) -> 'M[R]_(m, n1)).

Proof.

move=> u A /nbhs_ballP[e /= e0 eA].
apply/nbhs_ballP; exists e => //= v [_ uv]; apply: eA; split => // i j.
by apply: (le_lt_trans _ (uv i (lshift n2 j))); rewrite !mxE.
Qed.

Module

EndlessDenseTopologySource code

.
Import unstable.EndlessDense.

Section theory.
Local Open Scope order_scope.
Local Open Scope classical_set_scope.
Context {

dSource code

} {

TSource code

: orderTopologicalType d}.
Implicit Types (x y : T) (i : interval T).

Lemma

open_itv_open_endsSource code

iSource code

: is_endless T -> is_dense T -> neitv i ->
  open [set` i] -> itv_open_ends i.

Proof.

move=> T_endless T_dense.
case: i => l r /neitv_lt_bnd/= lr.
rewrite openE /interior/=.
(under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_open.
apply/negbNE/negP; case/(itv_open_endsPn lr) => x lrx.
have: x \in Interval l r.
  move: lr; case: lrx => ->; rewrite itv_boundlr lexx ?leBRight_ltBLeft//.
  by rewrite ltBRight_leBLeft => ->.
case/i_open => -[l' r'] [] + xj; rewrite -subset_itvP => /[swap].
have := xj; rewrite itv_boundlr => /andP[l'x xr'].
rewrite -subitvP//; first exact: xj.
rewrite subitvE => /andP[] ll' r'r.
apply/negP/itv_open_endsPn; [exact: (itv_boundlr_lt xj) | exists x].
move: l'x xr' ll' r'r.
by case: lrx => <-; [left|right]; apply/le_anti/andP; split.
Qed.

Lemma

closed_itv_closed_endsSource code

iSource code

: is_endless T -> is_dense T -> neitv i ->
  closed [set` i] -> itv_closed_ends i.

Proof.

move=> T_endless T_dense.
case: i => l r /neitv_lt_bnd/= lr.
rewrite closedE/= /prop_near1/=.
(under [X in X -> _]eq_forall do rewrite itv_nbhsE/=) => i_closed.
apply/negbNE/negP; case/(itv_closed_endsPn lr) => x lrx.
have: ~ (x \in Interval l r).
  by case: lrx => ->; rewrite itv_boundlr !bnd_simp// andbF.
apply; apply: i_closed => -[[l' r'][]] /itv_open_ends_boundlr -> /andP[] l'x xr'.
move: lr; case: lrx => -> => [xr|lx].
  have : BRight x < Order.min r r' by rewrite lt_min xr xr'.
  case/itv_bound_half_dense => // y /andP[] xy yr /(_ y); apply.
    rewrite /= itv_boundlr.
    have := yr; rewrite lt_min -!leBRight_ltBLeft => /andP[] _ ->.
    by rewrite andbT (le_trans _ xy)// ltW// ltBRight_leBLeft ltW.
  rewrite itv_boundlr xy/= leBRight_ltBLeft.
  by have := yr; rewrite lt_min => /andP[].
have : Order.max l l' < BLeft x by rewrite gt_max lx l'x.
case/itv_bound_half_dense => // y /andP[] ly yx /(_ y); apply.
  rewrite /= itv_boundlr.
  have := ly; rewrite ge_max => /andP[] _ -> /=.
  by rewrite leBRight_ltBLeft (lt_trans yx)// -leBRight_ltBLeft ltW.
rewrite itv_boundlr leBRight_ltBLeft yx andbT.
by have := ly; rewrite ge_max => /andP[].
Qed.

Let

itvoo_closureESource code

xSource code

ySource code

: is_endless T -> is_dense T -> neitv `]x, y[%O ->
  closure `]x, y[ = `[x, y].

Proof.

move=> T_endless T_dense /neitv_lt_bnd/= /[!bnd_simp] xy.
have ineq0 bb1 bb2 : neitv (Interval (BSide bb1 x) (BSide bb2 y)).
  have[z /andP[xz zy]]:= T_dense x y xy.
  apply/set0P; exists z; rewrite /= in_itv/=.
  by case: bb1; case: bb2; apply/andP; split; rewrite /= ?ltW.
have subcc : `]x, y[ `<=` `[x, y] by apply: subset_itv; rewrite !bnd_simp.
apply/seteqP; split.
  by rewrite (closure_id `[x, y]).1; [exact: itv_closed|exact: closureS].
rewrite (closureEbigcap_itvcc `[x, y])//; first exact: itv_closed.
rewrite setorder_itv_setDl_image// setDitvoo//.
rewrite powerset2 !image_setU !image_set1 setD0 setDitv1l setDitv1r setDitv_set2.
rewrite setIC !setIUl => /= z ? i -[[[]|]|] []->// ci.
all: exfalso; move/closed_itv_closed_ends: ci.
all: cbn; rewrite falseE; apply => //; exact: ineq0.
Qed.

Lemma

fin_itv_closureESource code

xSource code

ySource code

b1Source code

b2Source code

: is_endless T -> is_dense T ->
  neitv (Interval (BSide b1 x) (BSide b2 y)) ->
  closure [set` Interval (BSide b1 x) (BSide b2 y)] = `[x, y].

Proof.

move=> T_endless T_dense /neitv_lt_bnd/=  bxy.
have : x <= y by move: bxy; case: b1; case: b2; rewrite bnd_simp// => /ltW.
rewrite le_eqVlt => /orP[/eqP xy| xy].
  move: b1 b2 bxy; rewrite xy => -[][]; rewrite !bnd_simp// => _.
  by rewrite -((closure_id `[y,y]).1)//; exact: itv_closed.
apply/seteqP; split.
  rewrite (closure_id `[x, y]).1; first exact: itv_closed.
  by apply/closureS/subset_itv; rewrite !bnd_simp.
rewrite -itvoo_closureE//; last first.
  by apply/closureS/subset_itv; rewrite !bnd_simp.
have[z /andP[xz zy]]:= T_dense x y xy.
by apply/set0P; exists z; rewrite /= in_itv/= xz zy.
Qed.

Let

itvoy_closureESource code

xSource code

: is_endless T -> is_dense T ->
  closure `]x, +oo[ = `[x, +oo[.

Proof.

move=> T_endless T_dense.
have subcy : `]x, +oo[ `<=` `[x, +oo[.
  by apply: subset_itv => //; rewrite !bnd_simp.
apply/seteqP; split.
  rewrite (closure_id `[x, +oo[).1; last exact: closureS.
  exact: rray_closed.
rewrite (closureEbigcap_itvcc `[x, +oo[)//; first exact: rray_closed.
rewrite setorder_itv_setDl_image// setDitvoy.
  by apply/set0P; exists x; rewrite /= in_itv/= lexx.
rewrite powerset1 image_setU !image_set1 setD0 setDitv1l setIC setIUl.
move=> /= z/= zx /= i [] [] -> // ci; exfalso.
move/closed_itv_closed_ends: ci; cbn; rewrite falseE; apply => //.
have[_ [y xy]]:= T_endless x.
by apply/set0P; exists y; rewrite /= in_itv/= xy.
Qed.

Lemma

rinfty_itv_closureESource code

xSource code

bSource code

: is_endless T -> is_dense T ->
  closure [set` Interval (BSide b x) +oo] = `[x, +oo[.

Proof.

move=> T_endless T_dense.
have subcy: [set` Interval (BSide b x) +oo] `<=` `[x, +oo[.
  by apply: subset_itv => //; rewrite !bnd_simp.
apply/seteqP; split.
  rewrite (closure_id `[x, +oo[).1; last exact: closureS.
  exact: rray_closed.
rewrite -itvoy_closureE//.
by apply/closureS/subset_itv => //; rewrite !bnd_simp.
Qed.

Let

itvNyo_closureESource code

xSource code

: is_endless T -> is_dense T ->
  closure `]-oo, x[ = `]-oo, x].

Proof.

move=> T_endless T_dense.
have subcy : `]-oo, x[ `<=` `]-oo, x].
  by apply: subset_itv => //; rewrite !bnd_simp.
apply/seteqP; split.
  rewrite (closure_id `]-oo, x]).1; last exact: closureS.
  exact: lray_closed.
rewrite (closureEbigcap_itvcc `]-oo, x])//; first exact: lray_closed.
rewrite setorder_itv_setDl_image// setDitvNyo.
  by apply/set0P; exists x; rewrite /= in_itv/= lexx.
rewrite powerset1 image_setU !image_set1 setD0 setDitv1r setIC setIUl.
move=> /= z/= zx /= i [] [] -> // ci; exfalso.
move/closed_itv_closed_ends: ci; cbn; rewrite falseE; apply => //.
have[[y yx] _]:= T_endless x.
by apply/set0P; exists y; rewrite /= in_itv/= yx.
Qed.

Lemma

linfty_itv_closureESource code

xSource code

bSource code

: is_endless T -> is_dense T ->
  closure [set` Interval -oo (BSide b x)] = `]-oo, x].

Proof.

move=> T_endless T_dense.
have subNyc: [set` Interval -oo (BSide b x)] `<=` `]-oo, x].
  by apply: subset_itv => //; rewrite !bnd_simp.
apply/seteqP; split.
  rewrite (closure_id `]-oo, x]).1; last exact: closureS.
  exact: lray_closed.
rewrite -itvNyo_closureE//.
by apply/closureS/subset_itv => //; rewrite !bnd_simp.
Qed.

Lemma

rinfty_itv_interiorESource code

xSource code

bSource code

: is_endless T -> is_dense T ->
  [set` Interval (BSide b x) +oo]° = `]x, +oo[.

Proof.

move=> T_endless T_dense.
by apply: setC_inj; rewrite -closureC !setCitvr linfty_itv_closureE.
Qed.

Lemma

linfty_itv_interiorESource code

xSource code

bSource code

: is_endless T -> is_dense T ->
  [set` Interval -oo (BSide b x)]° = `]-oo, x[.

Proof.

move=> T_endless T_dense.
by apply: setC_inj; rewrite -closureC !setCitvl rinfty_itv_closureE.
Qed.

Lemma

fin_itv_interiorESource code

xSource code

ySource code

b1Source code

b2Source code

: is_endless T -> is_dense T ->
  [set` Interval (BSide b1 x) (BSide b2 y)]° = `]x, y[.

Proof.

move=> T_endless T_dense.
apply: setC_inj.
rewrite -closureC !setCitv/= closureU.
by rewrite linfty_itv_closureE// rinfty_itv_closureE.
Qed.

Lemma

itv_closureESource code

 (

lSource code

rSource code

: itv_bound T) :
    is_endless T -> is_dense T -> neitv (Interval l r) ->
  closure [set` Interval l r] =
  [set` Interval (match l with BSide _ x => BLeft x  | _ => l end)
                 (match r with BSide _ y => BRight y | _ => r end)].

Proof.

move=> T_endless T_dense.
move: l r => [[|] x | [|]] [[|] y | [|]] ineq0.
all: rewrite ?set_itv_infty_set0 ?closure0//.
all: rewrite ?set_itvNyy ?closureT//.
all: by rewrite (fin_itv_closureE, rinfty_itv_closureE, linfty_itv_closureE).
Qed.

Lemma

itv_interiorESource code

 (

lSource code

rSource code

: itv_bound T) : is_endless T -> is_dense T ->
  [set` Interval l r]° =
  [set` Interval (match l with BSide _ x => BRight x | _ => l end)
                 (match r with BSide _ y => BLeft y  | _ => r end)].

Proof.

move=> T_endless T_dense.
move: l r => [[|] x | [|]] [[|] y | [|]].
all: rewrite ?set_itv_infty_set0 ?interior0//.
all: rewrite ?set_itvNyy ?interiorT//.
all: by rewrite (fin_itv_interiorE, rinfty_itv_interiorE, linfty_itv_interiorE).
Qed.

End theory.

End EndlessDenseTopology.

Section realField_topology.
Context {

RSource code

: realFieldType}.
Implicit Type i : interval R.
Local Open Scope order_scope.

Let

real_is_endlessSource code

:= @EndlessDense.numDomain_is_endless R.
Let

real_is_denseSource code

:= @EndlessDense.numField_is_dense R.

Lemma

open_itv_open_endsSource code

iSource code

: neitv i -> open [set` i] -> itv_open_ends i.

Proof.

exact: EndlessDenseTopology.open_itv_open_ends. Qed.

Lemma

closed_itv_closed_endsSource code

iSource code

: neitv i -> closed [set` i] -> itv_closed_ends i.

Proof.

exact: EndlessDenseTopology.closed_itv_closed_ends. Qed.

Lemma

itv_closureEUsed by

• mathcomp.analysis.ftc

---

Source code

 (

lSource code

rSource code

: itv_bound R) : neitv (Interval l r) ->
  closure [set` Interval l r] =
  [set` Interval (match l with BSide _ x => BLeft x  | _ => l end)
                 (match r with BSide _ y => BRight y | _ => r end)].

Proof.

exact: EndlessDenseTopology.itv_closureE. Qed.

Lemma

itv_interiorESource code

 (

lSource code

rSource code

: itv_bound R) :
  [set` Interval l r]° =
  [set` Interval (match l with BSide _ x => BRight x | _ => l end)
                 (match r with BSide _ y => BLeft y  | _ => r end)].

Proof.

exact: EndlessDenseTopology.itv_interiorE. Qed.

End realField_topology.