Module mathcomp.analysis.topology_theory.metric_structure

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval_inference rat interval zmodp vector.
From mathcomp Require Import fieldext falgebra archimedean finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets contra reals.
From mathcomp Require Import topology_structure uniform_structure
  pseudometric_structure num_topology product_topology separation_axioms.


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

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

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HBSource code

.

mixinSource code

RecordSource code

PseudoMetric_isMetricSource code

 (

KSource code

:Source code

numDomainTypeSource code

) M & PseudoMetric K M := {
  mdist : M -> M -> K ;
  mdist_ge0 : forall

xSource code

ySource code

, 0 <= mdist x y ;
  mdist_positivity : forall

xSource code

ySource code

, mdist x y = 0 -> x = y;
  ballEmdist : forall

xSource code

dSource code

, ball x d = [set

ySource code

| mdist x y < d]
}.

#[shortUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

(

type=Used by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

"metricType"Used by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

)

]Used by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

HBUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

.

structureUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

DefinitionUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

MetricUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

 (

KUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

:Used by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

numDomainTypeUsed by

• mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule

---

Source code

) :=
  {

MSource code

of PseudoMetric K M & PseudoMetric_isMetric K M }.

Section metric_numDomainType.
Context {

RSource code

: numDomainType} (

TSource code

: metricType R).

Let

distSource code

:= @mdist R T.

Lemma

metric_symSource code

xSource code

ySource code

: dist x y = dist y x.

Proof.

have cxy : dist x y >=< dist y x.
  by apply: real_comparable; apply: ger0_real; exact: mdist_ge0.
apply/eqP; rewrite eq_le; apply/andP; split.
- rewrite comparable_leNgt//; apply/negP => xy.
  have := @ball_sym _ _ y x (dist x y); rewrite !ballEmdist/= => /(_ xy).
  by rewrite ltxx.
- rewrite comparable_leNgt//; first by rewrite comparable_sym.
  apply/negP => xy.
  have := @ball_sym _ _ x y (dist y x); rewrite !ballEmdist/= => /(_ xy).
  by rewrite ltxx.
Qed.

Lemma

mdistxxSource code

xSource code

: dist x x = 0.

Proof.

have := mdist_ge0 x x.
rewrite /dist le_eqVlt => /predU1P[<-//|].
by move/(ballxx x); rewrite ballEmdist /= ltxx.
Qed.

Lemma

mdist_gt0Source code

xSource code

ySource code

: (0 < dist x y) = (x != y).

Proof.

rewrite lt_neqAle mdist_ge0 andbT.
apply/negPn/negPn => [/eqP/esym/mdist_positivity/eqP//|/eqP ->].
by rewrite [eqbRHS]mdistxx.
Qed.

End metric_numDomainType.

Section metric_numFieldType.
Context {

RSource code

: numFieldType} (

TSource code

: metricType R).

Let

distSource code

:= @mdist R T.

Lemma

metric_triangleSource code

xSource code

ySource code

zSource code

: dist x z <= dist x y + dist y z.

Proof.

have c : dist x z >=< dist x y + dist y z.
  by rewrite real_comparable// ger0_real ?addr_ge0// mdist_ge0.
rewrite (comparable_leNgt c); apply/negP => xy.
set e := dist x z - (dist x y + dist y z).
have e0 : 0 < e by rewrite subr_gt0.
have e20 : 0 < e / 2 by rewrite divr_gt0.
have xe2y : ball x (dist x y + e / 2) y by rewrite ballEmdist/= ltrDl.
have ye2z : ball y (dist y z + e / 2) z by rewrite ballEmdist/= ltrDl.
have := ball_triangle xe2y ye2z.
by rewrite ballEmdist/= addrACA -splitr subrKC ltxx.
Qed.

Lemma

metric_hausdorffSource code

: hausdorff_space T.

Proof.

move=> p q pq; absurd_not => qp; move: pq.
pose D := dist p q / 2; have D0 : 0 < D.
  by rewrite divr_gt0// mdist_gt0.
have p2Dq : ~ ball p (dist p q) q by rewrite ballEmdist/= ltxx.
move=> /(_ (ball p _) (ball q _) (nbhsx_ballx _ _ D0) (nbhsx_ballx _ _ D0)).
move/set0P/eqP; apply; rewrite -subset0 => x [pDx /ball_sym qDx].
by have := ball_triangle pDx qDx; rewrite -splitr.
Qed.

End metric_numFieldType.

Section prod_metric.
Context {

KSource code

: numDomainType} (

TSource code

USource code

: metricType K).

Let

MSource code

:= (T * U)%type.

Let

cmpSource code

 (

xSource code

ySource code

: M) : mdist x.1 y.1 >=< mdist x.2 y.2.

Proof.

by apply: real_comparable; apply: ger0_real; exact: mdist_ge0. Qed.

Definition

prod_mdist

---

Source code

 (

xSource code

ySource code

: M) := maxr (mdist x.1 y.1) (mdist x.2 y.2).

Let

prod_mdist_ge0Source code

xSource code

ySource code

: 0 <= prod_mdist x y.

Proof.

by rewrite /prod_mdist comparable_le_max// mdist_ge0. Qed.

Let

prod_mdist_positivitySource code

xSource code

ySource code

: prod_mdist x y = 0 -> x = y.

Proof.

rewrite /prod_mdist /= => m0.
have le01 : mdist x.1 y.1 <= 0 by rewrite -m0 comparable_le_max// lexx.
have le02 : mdist x.2 y.2 <= 0 by rewrite -m0 comparable_le_max// lexx orbT.
have eq01 : mdist x.1 y.1 = 0 by apply/le_anti; rewrite le01 mdist_ge0.
have eq02 : mdist x.2 y.2 = 0 by apply/le_anti; rewrite le02 mdist_ge0.
rewrite (surjective_pairing x) (surjective_pairing y).
by congr pair; exact: mdist_positivity.
Qed.

Let

ballEprod_mdistSource code

xSource code

dSource code

: ball x d = [set

ySource code

| prod_mdist x y < d].

Proof.

apply/seteqP; split => [y []|y /= xyd].
  rewrite !ballEmdist/= /prod_mdist => b1 b2.
  by rewrite comparable_gt_max// b1 b2.
rewrite /ball/= /prod_ball/= !ballEmdist/=.
by apply/andP; rewrite -comparable_gt_max.
Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

PseudoMetric_isMetricSource code

.Build K (T * U)%type
  prod_mdist_ge0 prod_mdist_positivity ballEprod_mdist.

End prod_metric.

HBSource code

.

factorySource code

RecordSource code

isMetricSource code

 (

KSource code

:Source code

numFieldTypeSource code

) (M : Type) & Choice M := {
  mdist : M -> M -> K ;
  mdistxx : forall

xSource code

, mdist x x = 0 ;
  mdist_positivity : forall

xSource code

ySource code

, mdist x y = 0 -> x = y ;
  mdist_sym : forall

xSource code

ySource code

, mdist x y = mdist y x ;
  mdist_triangle : forall

ySource code

xSource code

zSource code

, mdist x z <= mdist x y + mdist y z
}.

HBSource code

.

buildersSource code

ContextSource code

KSource code

MSource code

&Source code

isMetricSource code

K M.

Let

ballSource code

 (

xSource code

: M)

eSource code

: set M := [set

ySource code

| mdist x y < e].

Let

entSource code

: set_system (M * M) := entourage_ ball.

Let

nbhsSource code

 (

xSource code

: M) : set_system M := nbhs_ ent x.

Let

nbhsESource code

: nbhs = nbhs_ ent

Proof.

by []. Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

hasNbhsSource code

.Build M nbhs.

Let

ball_centerSource code

xSource code

 (

eSource code

: K) : 0 < e -> ball x e x.

Proof.

by move=> e0; rewrite /ball/= mdistxx. Qed.

Let

ball_symSource code

xSource code

ySource code

 (

eSource code

: K) : ball x e y -> ball y e x.

Proof.

by rewrite /ball/= mdist_sym. Qed.

Let

ball_triangleSource code

xSource code

ySource code

zSource code

e1Source code

e2Source code

: ball x e1 y -> ball y e2 z ->
  ball x (e1 + e2) z.

Proof.

by rewrite /ball/= => ? ?; rewrite (le_lt_trans (mdist_triangle y _ _))// ltrD.
Qed.

Let

entourageESource code

: ent = entourage_ ball

Proof.

by []. Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

@Nbhs_isPseudoMetricSource code

.Build K M
  ent nbhsE ball ball_center ball_sym ball_triangle entourageE.

Let

mdist_ge0Source code

xSource code

ySource code

: 0 <= mdist x y.

Proof.

rewrite -(@pmulrn_lge0 _ _ 2)// -(mdistxx x).
by rewrite (le_trans (mdist_triangle y _ _))// mdist_sym -mulr2n.
Qed.

Let

ballEmdistSource code

xSource code

dSource code

: ball x d = [set

ySource code

| mdist x y < d]

Proof.

by []. Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

PseudoMetric_isMetricSource code

.Build K M
  mdist_ge0 mdist_positivity ballEmdist.

HBSource code

.

endSource code

.

Section numFieldType_metric.
Context {

RSource code

: numFieldType}.
Implicit Type x y : R.

Let

distSource code

xSource code

ySource code

:= `|y - x|.

Let

dist_ge0Source code

xSource code

ySource code

: 0 <= dist x y.

Proof.

exact: normr_ge0. Qed.

Let

dist_positivitySource code

xSource code

ySource code

: dist x y = 0 -> x = y.

Proof.

by move/normr0_eq0/eqP; rewrite subr_eq0 => /eqP. Qed.

Let

ballEmdistSource code

xSource code

dSource code

: ball x d = [set

ySource code

| dist x y < d].

Proof.

by apply/seteqP; split => [|]/= A; rewrite /ball/= distrC. Qed.

HBSource code

.

instanceSource code

DefinitionSource code

_Source code

:=Source code

  

@PseudoMetric_isMetricSource code

.Build R R^o dist dist_ge0 dist_positivity ballEmdist.

End numFieldType_metric.

Module

metricType_numDomainTypeSource code

.
Section metricType_numDomainType.
Context {

KSource code

: numDomainType} {

VSource code

: metricType K}.

Local Notation

ball_mdistSource code

:= (fun

xSource code

dSource code

=> [set

ySource code

: V | mdist x y < d]).

Lemma

ball_mdistESource code

: ball_mdist = ball.

Proof.

by apply/funext => x; apply/funext=> d; rewrite - ballEmdist. Qed.

Local Notation

nbhs_mdistSource code

:= (nbhs_ball_ ball_mdist).

Lemma

nbhs_nbhs_mdistSource code

: nbhs_mdist = nbhs.

Proof.

apply/funext => x.
rewrite /nbhs_ball_.
rewrite -filter_from_ballE.
by rewrite -ball_mdistE.
Qed.

Lemma

nbhs_mdistPSource code

xSource code

 (

PSource code

: V -> Prop) : (\near

xSource code

, P x) <-> nbhs_mdist x P.

Proof.

by rewrite nbhs_nbhs_mdist. Qed.

Lemma

filter_from_mdist_nbhsSource code

 (

ySource code

: V) :
  filter_from (fun

iSource code

: K => 0 < i) (fun (

iSource code

: K) (

y'Source code

: V) => mdist y y' < i)
  = nbhs y.

Proof.

rewrite -filter_from_ballE; apply/seteqP; split => [A|A]/=.
  by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist.
by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist in yxA.
Qed.

Let

nbhs_simplSource code

:= (nbhs_simpl,@nbhs_nbhs_mdist,@filter_from_mdist_nbhs).

Lemma

fcvgrPdist_ltSource code

{

FSource code

: set_system V} {

FFSource code

: Filter F} (

ySource code

: V) :
  F --> y <-> forall

epsSource code

, 0 < eps -> \forall

y'Source code

\near F, mdist y y' < eps.

Proof.

by rewrite -filter_fromP/= !nbhs_simpl. Qed.

Lemma

cvgrPdist_ltUsed by

• mathcomp.analysis.ereal

---

Source code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> V) (

ySource code

: V) :
  f @ F --> y <-> forall

epsSource code

, 0 < eps -> \forall

tSource code

\near F, mdist y (f t) < eps.

Proof.

exact: fcvgrPdist_lt. Qed.

Lemma

cvgr_dist_ltUsed by

• mathcomp.analysis.ereal

---

Source code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> V) (

ySource code

: V) :
  f @ F --> y -> forall

epsSource code

, eps > 0 -> \forall

tSource code

\near F, mdist y (f t) < eps.

Proof.

by move=> /cvgrPdist_lt. Qed.

Lemma

cvgr_dist_leSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> V) (

ySource code

: V) :
  f @ F --> y -> forall

epsSource code

, eps > 0 -> \forall

tSource code

\near F, mdist y (f t) <= eps.

Proof.

by move=> ? ? ?; near do rewrite ltW//; apply: cvgr_dist_lt.
Unshelve. all: by end_near. Qed.

End metricType_numDomainType.

Section at_left_right_metricType.
Variables (

RSource code

: numFieldType) (

VSource code

: metricType R).

Lemma

nbhsr0PSource code

 (

PSource code

: set V)

xSource code

:
  (\forall

ySource code

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

eSource code

\near 0^'+, forall

ySource code

, mdist x y <= e -> P y).

Proof.

rewrite (*nbhs0P*)/= near_withinE !near_simpl.
split.
  move => /nbhs_mdistP[/= _/posnumP[e] /(_ _) Px].
  apply/(@nbhs_mdistP R R^o).
  exists e%:num => //= r /= re yr y xyr.
  apply: Px => /=.
  rewrite (le_lt_trans _ re)//.
  rewrite (le_trans xyr)//.
  by rewrite /mdist/= subr0 real_ler_norm// gtr0_real.
move => /(@nbhs_mdistP R R^o)[/= _/posnumP[e] /(_ _) Px].
apply/(@nbhs_mdistP R V).
exists (e%:num / 2) => //= r /= re; apply: (Px (e%:num / 2)) => //=.
  by rewrite /mdist/= subr0 gtr0_norm// ltr_pdivrMr// ltr_pMr// ltr1n.
by rewrite ltW.
Qed.

Let

cvgrPSource code

{

FSource code

: set_system V} {

FFSource code

: Filter F} (

ySource code

: V) : [<->
  F --> y;
  forall

epsSource code

, 0 < eps -> \forall

tSource code

\near F, mdist y t <= eps;
  \forall

epsSource code

\near 0^'+, \forall

tSource code

\near F, mdist y t <= eps;
  \forall

epsSource code

\near 0^'+, \forall

tSource code

\near F, mdist y t < eps].

Proof.

tfae; first by move=> *; apply: cvgr_dist_le.
- by move=> Fy; near do apply: Fy; apply: nbhs_right_gt.
- move=> Fy; near=> e; near (0:R)^'+ => d; near=> x.
  rewrite (@le_lt_trans _ _ d)//; first by near: x; near: d.
  by near: d; apply: nbhs_right_lt; near: e; apply: nbhs_right_gt.
- move=> Fy; apply/cvgrPdist_lt => e e_gt0; near (0:R)^'+ => d.
  near=> x; rewrite (@lt_le_trans _ _ d)//; first by near: x; near: d.
  by near: d; apply: nbhs_right_le.
Unshelve. all: by end_near. Qed.

Lemma

cvgrPdist_leUsed by

• mathcomp.analysis.topology_theory.edist

---

Source code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> V) (

ySource code

: V) :
  f @ F --> y <-> forall

epsSource code

, 0 < eps -> \forall

tSource code

\near F, mdist y (f t) <= eps.

Proof.

exact: (cvgrP _ 0 1)%N. Qed.

End at_left_right_metricType.

End metricType_numDomainType.

Section at_left_rightR.
Variable (

RSource code

: numFieldType).

Let

cvgrPdistC_ltSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R^o) (

ySource code

: R) :
  f @ F --> y <-> forall

epsSource code

, 0 < eps -> \forall

tSource code

\near F, mdist (f t) y < eps.

Proof.

rewrite metricType_numDomainType.cvgrPdist_lt.
by under eq_forall do under eq_near do rewrite /mdist/= (@distrC _ R^o).
Qed.

Let

cvgr_distC_ltSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R^o) (

ySource code

: R) :
  f @ F --> y -> forall

epsSource code

, eps > 0 -> \forall

tSource code

\near F, mdist (f t) y < eps.

Proof.

by move=> /cvgrPdistC_lt. Qed.

Lemma

real_cvgr_ltSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R) (

ySource code

: R) :
    y \is Num.real -> f @ F --> y ->
  forall

zSource code

, z > y -> \forall

tSource code

\near F, f t \is Num.real -> f t < z.

Proof.

move=> yr Fy z zy; near=> x => fxr.
rewrite -(ltrD2r (- y)) real_ltr_normlW// ?rpredB// distrC.
by near: x; apply: cvgr_distC_lt => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma

real_cvgr_leSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R) (

ySource code

: R) :
    y \is Num.real ->  f @ F --> y ->
  forall

zSource code

, z > y -> \forall

tSource code

\near F, f t \is Num.real -> f t <= z.

Proof.

move=> /real_cvgr_lt/[apply] + ? z0 => /(_ _ z0).
by apply: filterS => ? /[apply]/ltW.
Qed.

Lemma

real_cvgr_gtSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R) (

ySource code

: R) :
    y \is Num.real -> f @ F --> y ->
  forall

zSource code

, y > z -> \forall

tSource code

\near F, f t \is Num.real -> f t > z.

Proof.

move=> yr Fy z zy; near=> x => fxr.
rewrite -ltrN2 -(ltrD2l y) real_ltr_normlW// ?rpredB// distrC.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma

real_cvgr_geSource code

{

TSource code

} {

FSource code

: set_system T} {

FFSource code

: Filter F} (

fSource code

: T -> R) (

ySource code

: R) :
    y \is Num.real -> f @ F --> y ->
  forall

zSource code

, z < y -> \forall

tSource code

\near F, f t \is Num.real -> f t >= z.

Proof.

move=> /real_cvgr_gt/[apply] + ? z0 => /(_ _ z0).
by apply: filterS => ? /[apply]/ltW.
Qed.

End at_left_rightR.
Arguments real_cvgr_le {R T F FF f}.
Arguments real_cvgr_lt {R T F FF f}.
Arguments real_cvgr_ge {R T F FF f}.
Arguments real_cvgr_gt {R T F FF f}.

Section squeeze_cvgr.
Context {

TSource code

: Type} {

FSource code

: set_system T} {

FFSource code

: Filter F} {

RSource code

: realFieldType}.
Implicit Types f g h : T -> R.

Lemma

cvgr_ltUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.derive
• mathcomp.analysis.realfun

---

Source code

fSource code

 (

ySource code

: R) :
  f @ F --> y -> forall

zSource code

, z > y -> \forall

tSource code

\near F, f t < z.

Proof.

move=> Fy z zy; near=> x; rewrite -(ltrD2r (- y)) ltr_normlW//.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma

cvgr_gtUsed by

• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.realfun

---

Source code

fSource code

 (

ySource code

: R) :
  f @ F --> y -> forall

zSource code

, y > z -> \forall

tSource code

\near F, f t > z.

Proof.

move=> Fy z zy; near=> x; rewrite -ltrN2 -(ltrD2l y) ltr_normlW// distrC.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma

cvgr_leUsed by

• mathcomp.analysis.derive

---

Source code

fSource code

 (

ySource code

: R) :
  f @ F --> y -> forall

zSource code

, z > y -> \forall

tSource code

\near F, f t <= z.

Proof.

by move=> /cvgr_lt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
Qed.

Lemma

cvgr_geUsed by

• mathcomp.analysis.normedtype_theory.normed_module

---

Source code

fSource code

 (

ySource code

: R) :
  f @ F --> y -> forall

zSource code

, z < y -> \forall

tSource code

\near F, f t >= z.

Proof.

by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
Qed.

Lemma

squeeze_cvgrUsed by

• mathcomp.analysis.sequences
• mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under
• mathcomp.analysis.gauss_integral
• mathcomp.analysis.normedtype_theory.normed_module
• mathcomp.analysis.normedtype_theory.tvs

---

Source code

fSource code

gSource code

hSource code

: (\near

FSource code

, f F <= g F <= h F) ->
  forall

lSource code

: R, f @ F --> l -> h @ F --> l -> g @ F --> l.

Proof.

move=> fgh l lfa lga.
apply/(@metricType_numDomainType.cvgrPdist_lt R R^o) => e e_gt0.
near=> x; have /(_ _)/andP[//|fg gh] := near fgh x.
rewrite ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=.
  by near: x; apply: (cvgr_gt lfa); rewrite // gtrDl oppr_lt0.
by near: x; apply: (cvgr_lt lga); rewrite // ltrDl.
Unshelve. all: end_near. Qed.

End squeeze_cvgr.
Arguments cvgr_lt {T F FF R f}.
Arguments cvgr_gt {T F FF R f}.
Arguments cvgr_le {T F FF R f}.
Arguments cvgr_ge {T F FF R f}.
Arguments squeeze_cvgr {T F FF R} f g h.