Module mathcomp.analysis.topology_theory.edist
From HB Require Import structures.From mathcomp Require Import boot order finmap ssralg ssrnum.
From mathcomp Require Import interval interval_inference archimedean.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import set_interval reals topology_structure
pseudometric_structure num_topology product_topology metric_structure
separation_axioms ereal.
# Extended distance function
```
edist == the extended distance function for a
pseudometric X, from X * X -> \bar R
edist_inf A == the infimum of distances to the set A
```
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 pseudoMetricDist.
Context {RSource code : realType} {XSource code : pseudoMetricType R}.
Implicit Types r : R.
Definition edist
Source code (xySource code : X * X) : \bar R :=
ereal_inf (EFin @` [set rSource code | 0 < r /\ ball xy.1 r xy.2]).
Lemma edist_ge0Used by
- mathcomp.analysis.normedtype_theory.urysohn
Source code (xySource code : X * X) : (0 <= edist xy)%E.
Proof.
Lemma edist_neqNySource code (xySource code : X * X) : (edist xy != -oo)%E.
Proof.
Lemma edist_lt_ballUsed by
- mathcomp.analysis.normedtype_theory.urysohn
Source code rSource code (xySource code : X * X) : (edist xy < r%:E)%E -> ball xy.1 r xy.2.
Proof.
case/ereal_inf_lt => ? [+ []] => _/posnumP[eps] bxye <-; rewrite lte_fin.
by move/ltW/le_ball; exact.
Qed.
by move/ltW/le_ball; exact.
Qed.
Lemma edist_finSource code rSource code (xySource code : X * X) :
0 < r -> ball xy.1 r xy.2 -> (edist xy <= r%:E)%E.
Proof.
move: r => _/posnumP[r] => ?; rewrite -(ereal_inf1 r%:num%:E) ereal_inf_le_tmp//.
by move=> ? -> /=; exists r%:num; split.
Qed.
by move=> ? -> /=; exists r%:num; split.
Qed.
Lemma edist_pinftyPSource code (xySource code : X * X) :
(edist xy = +oo)%E <-> (forall rSource code, 0 < r -> ~ ball xy.1 r xy.2).
Proof.
split.
move/ereal_inf_pinfty => xrb r rpos rb; move: (ltry r); rewrite ltey => /eqP.
by apply; apply: xrb; exists r.
rewrite /edist=> nrb; suff -> : [set rSource code | 0 < r /\ ball xy.1 r xy.2] = set0.
by rewrite image_set0 ereal_inf0.
by rewrite -subset0 => r [?] rb; apply: nrb; last exact: rb.
Qed.
move/ereal_inf_pinfty => xrb r rpos rb; move: (ltry r); rewrite ltey => /eqP.
by apply; apply: xrb; exists r.
rewrite /edist=> nrb; suff -> : [set rSource code | 0 < r /\ ball xy.1 r xy.2] = set0.
by rewrite image_set0 ereal_inf0.
by rewrite -subset0 => r [?] rb; apply: nrb; last exact: rb.
Qed.
Lemma edist_finPUsed by
- mathcomp.analysis.normedtype_theory.urysohn
Source code (xySource code : X * X) :
(edist xy \is a fin_num)%E <-> exists2 rSource code, 0 < r & ball xy.1 r xy.2.
Proof.
Lemma edist_fin_openSource code : open [set xySource code : X * X | edist xy \is a fin_num].
Proof.
move=> z /= /edist_finP [] _/posnumP[r] bzr.
exists (ball z.1 r%:num, ball z.2 r%:num); first by split; exact: nbhsx_ballx.
case=> a b [bza bzb]; apply/edist_finP; exists (r%:num + r%:num + r%:num) => //.
exact/(ball_triangle _ bzb)/(ball_triangle _ bzr)/ball_sym.
Qed.
exists (ball z.1 r%:num, ball z.2 r%:num); first by split; exact: nbhsx_ballx.
case=> a b [bza bzb]; apply/edist_finP; exists (r%:num + r%:num + r%:num) => //.
exact/(ball_triangle _ bzb)/(ball_triangle _ bzr)/ball_sym.
Qed.
Lemma edist_fin_closedSource code : closed [set xySource code : X * X | edist xy \is a fin_num].
Proof.
move=> z /= /(_ (ball z 1)) []; first exact: nbhsx_ballx.
move=> w [/edist_finP [] _/posnumP[r] babr [bz1w1 bz2w2]]; apply/edist_finP.
exists (1 + (r%:num + 1)) => //.
exact/(ball_triangle bz1w1)/(ball_triangle babr)/ball_sym.
Qed.
move=> w [/edist_finP [] _/posnumP[r] babr [bz1w1 bz2w2]]; apply/edist_finP.
exists (1 + (r%:num + 1)) => //.
exact/(ball_triangle bz1w1)/(ball_triangle babr)/ball_sym.
Qed.
Lemma edist_pinfty_openSource code : open [set xySource code : X * X | edist xy = +oo]%E.
Proof.
rewrite -closedC; have := edist_fin_closed; congr (_ _).
by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE// ltey => /eqP.
Qed.
by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE// ltey => /eqP.
Qed.
Lemma edist_symSource code (xSource code ySource code : X) : edist (x, y) = edist (y, x).
Lemma edist_triangleSource code (xSource code ySource code zSource code : X) :
(edist (x, z) <= edist (x, y) + edist (y, z))%E.
Proof.
have [->|] := eqVneq (edist (x, y)) +oo%E; first by rewrite addye ?leey.
have [->|] := eqVneq (edist (y, z)) +oo%E; first by rewrite addey ?leey.
rewrite -?ltey -?ge0_fin_numE//.
move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy].
have [|] := eqVneq (edist (x, z)) +oo%E.
move/edist_pinftyP /(_ (r1%:num + r2%:num) _) => -[//|].
exact: (ball_triangle xy).
rewrite -ltey -ge0_fin_numE// => /[dup] xzfin.
move/edist_finP => [_/posnumP[del] /= xz].
rewrite /edist /= ?ereal_inf_EFin.
- by exists 0 => ? /= [/ltW].
- by exists (r1%:num + r2%:num); split => //; apply: (ball_triangle xy).
- by exists 0 => ? /= [/ltW].
- by exists r1%:num; split.
- by exists 0 => ? /= [/ltW].
- by exists r2%:num; split.
rewrite -EFinD lee_fin -inf_sumE //.
- by split; [exists r1%:num; split| exists 0 => ? /= [/ltW]].
- by split; [exists r2%:num; split| exists 0 => ? /= [/ltW]].
apply: lb_le_inf.
by exists (r1%:num + r2%:num); exists r1%:num => //; exists r2%:num.
move=> ? [+ []] => _/posnumP[p] xpy [+ []] => _/posnumP[q] yqz <-.
apply: ge_inf; first by exists 0 => ? /= [/ltW].
by split => //; exact: (ball_triangle xpy).
Qed.
have [->|] := eqVneq (edist (y, z)) +oo%E; first by rewrite addey ?leey.
rewrite -?ltey -?ge0_fin_numE//.
move=> /edist_finP [_/posnumP[r2] /= yz] /edist_finP [_/posnumP[r1] /= xy].
have [|] := eqVneq (edist (x, z)) +oo%E.
move/edist_pinftyP /(_ (r1%:num + r2%:num) _) => -[//|].
exact: (ball_triangle xy).
rewrite -ltey -ge0_fin_numE// => /[dup] xzfin.
move/edist_finP => [_/posnumP[del] /= xz].
rewrite /edist /= ?ereal_inf_EFin.
- by exists 0 => ? /= [/ltW].
- by exists (r1%:num + r2%:num); split => //; apply: (ball_triangle xy).
- by exists 0 => ? /= [/ltW].
- by exists r1%:num; split.
- by exists 0 => ? /= [/ltW].
- by exists r2%:num; split.
rewrite -EFinD lee_fin -inf_sumE //.
- by split; [exists r1%:num; split| exists 0 => ? /= [/ltW]].
- by split; [exists r2%:num; split| exists 0 => ? /= [/ltW]].
apply: lb_le_inf.
by exists (r1%:num + r2%:num); exists r1%:num => //; exists r2%:num.
move=> ? [+ []] => _/posnumP[p] xpy [+ []] => _/posnumP[q] yqz <-.
apply: ge_inf; first by exists 0 => ? /= [/ltW].
by split => //; exact: (ball_triangle xpy).
Qed.
Lemma edist_continuousSource code : continuous edist.
Proof.
move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E.
rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xySource code | edist xy = +oo]%E).
by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->.
by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open.
rewrite -ltey -ge0_fin_numE// => efin.
rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin.
by have := edist_fin_open efin; apply: filter_app; near=> w.
apply/(@metricType_numDomainType.cvgrPdist_le _ R^o) => _/posnumP[eps]/=.
suff: \forall tSource code \near (nbhs x, nbhs y),
@mdist _ R^o (fine (edist (x, y))) (fine (edist t)) <= eps%:num.
by [].
rewrite -near2_pair; near=> a b => /=.
have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E.
rewrite (edist_sym x a) -addeA.
by rewrite (le_trans (@edist_triangle _ x _)) ?leeD ?edist_triangle.
have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E.
rewrite (edist_sym y b) -addeA.
by rewrite (le_trans (@edist_triangle _ a _))// ?leeD// ?edist_triangle.
have xafin : edist (x, a) \is a fin_num.
by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx.
have ybfin : edist (y, b) \is a fin_num.
by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx.
have abfin : edist (a, b) \is a fin_num.
by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE.
have xyabfin : (edist (x, y) - edist (a, b))%E \is a fin_num
by rewrite fin_numB abfin efin.
rewrite /mdist/= distrC.
rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//.
rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first.
by rewrite [eps%:num]splitr/= EFinD leeD//; apply: edist_fin => //=;
[near: a | near: b]; exact: nbhsx_ballx.
have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)).
by rewrite gee0_abs ?subre_ge0// leeBlDr// addeAC.
rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//.
by rewrite addeC leeBlDr// addeAC.
Unshelve. all: end_near. Qed.
rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xySource code | edist xy = +oo]%E).
by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->.
by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open.
rewrite -ltey -ge0_fin_numE// => efin.
rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin.
by have := edist_fin_open efin; apply: filter_app; near=> w.
apply/(@metricType_numDomainType.cvgrPdist_le _ R^o) => _/posnumP[eps]/=.
suff: \forall tSource code \near (nbhs x, nbhs y),
@mdist _ R^o (fine (edist (x, y))) (fine (edist t)) <= eps%:num.
by [].
rewrite -near2_pair; near=> a b => /=.
have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E.
rewrite (edist_sym x a) -addeA.
by rewrite (le_trans (@edist_triangle _ x _)) ?leeD ?edist_triangle.
have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E.
rewrite (edist_sym y b) -addeA.
by rewrite (le_trans (@edist_triangle _ a _))// ?leeD// ?edist_triangle.
have xafin : edist (x, a) \is a fin_num.
by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx.
have ybfin : edist (y, b) \is a fin_num.
by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx.
have abfin : edist (a, b) \is a fin_num.
by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE.
have xyabfin : (edist (x, y) - edist (a, b))%E \is a fin_num
by rewrite fin_numB abfin efin.
rewrite /mdist/= distrC.
rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//.
rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first.
by rewrite [eps%:num]splitr/= EFinD leeD//; apply: edist_fin => //=;
[near: a | near: b]; exact: nbhsx_ballx.
have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)).
by rewrite gee0_abs ?subre_ge0// leeBlDr// addeAC.
rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//.
by rewrite addeC leeBlDr// addeAC.
Unshelve. all: end_near. Qed.
Lemma edist_closePSource code xSource code ySource code : close x y <-> edist (x, y) = 0%E.
Proof.
rewrite ball_close; split=> [bxy|edist0 eps]; first last.
by apply: (@edist_lt_ball _ (x, y)); rewrite edist0.
case: ltgtP (edist_ge0 (x, y)) => // dpos _.
have xxfin : edist (x, y) \is a fin_num.
rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin//.
exact: bxy (widen_itv 1%:itv).
have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK.
pose eps := PosNum dpose.
have : (edist (x, y) <= (eps%:num / 2)%:E)%E.
apply: ereal_inf_lbound; exists (eps%:num / 2) => //; split => //.
exact: (bxy (eps%:num / 2)%:pos).
apply: contra_leP => _.
by rewrite /= EFinM fineK// lte_pdivrMr// lte_pmulr// lte1n.
Qed.
by apply: (@edist_lt_ball _ (x, y)); rewrite edist0.
case: ltgtP (edist_ge0 (x, y)) => // dpos _.
have xxfin : edist (x, y) \is a fin_num.
rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin//.
exact: bxy (widen_itv 1%:itv).
have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK.
pose eps := PosNum dpose.
have : (edist (x, y) <= (eps%:num / 2)%:E)%E.
apply: ereal_inf_lbound; exists (eps%:num / 2) => //; split => //.
exact: (bxy (eps%:num / 2)%:pos).
apply: contra_leP => _.
by rewrite /= EFinM fineK// lte_pdivrMr// lte_pmulr// lte1n.
Qed.
Lemma edist_reflSource code xSource code : edist (x, x) = 0%E
Proof.
exact/edist_closeP. Qed.
Lemma edist_closelSource code xSource code ySource code zSource code : close x y -> edist (x, z) = edist (y, z).
Proof.
move=> /edist_closeP xy0; apply: le_anti; apply/andP; split.
by rewrite -[edist (y, z)]add0e -xy0 edist_triangle.
by rewrite -[edist (x, z)]add0e -xy0 [edist (x, y)]edist_sym edist_triangle.
Qed.
by rewrite -[edist (y, z)]add0e -xy0 edist_triangle.
by rewrite -[edist (x, z)]add0e -xy0 [edist (x, y)]edist_sym edist_triangle.
Qed.
End pseudoMetricDist.
#[global]
Hint Extern 0 (is_true (0%R <= edist _)%E) => solve [apply: edist_ge0] : core.
#[global]
Hint Extern 0 (is_true (edist _ != -oo%E)) => solve [apply: edist_neqNy] : core.
Section edist_inf.
Context {RSource code : realType} {TSource code : pseudoMetricType R} (ASource code : set T).
Definition edist_inf
edist : forall {R : realType} {X : pseudoMetricType R}, X * X -> \bar R edist is not universe polymorphic Arguments edist {R X} xy edist is transparent Expands to: Constant mathcomp.analysis.topology_theory.edist.edist Declared in library mathcomp.analysis.topology_theory.edist, line 37, characters 11-16
Used by
- mathcomp.analysis.normedtype_theory.urysohn
Source code zSource code := ereal_inf [set edist (z, a) | aSource code in A].
Lemma edist_inf_ge0Used by
- mathcomp.analysis.normedtype_theory.urysohn
Source code wSource code : (0 <= edist_inf w)%E.
Proof.
Lemma edist_inf_neqNySource code wSource code : (edist_inf w != -oo)%E.
Proof.
Lemma edist_inf_triangleSource code xSource code ySource code : (edist_inf x <= edist (x, y) + edist_inf y)%E.
Proof.
have [A0|/set0P[a0 Aa0]] := eqVneq A set0.
by rewrite /edist_inf A0 ?image_set0 ?ereal_inf0 addey.
have [fyn|] := boolP (edist_inf y \is a fin_num); first last.
by rewrite ge0_fin_numE// ?ltey negbK => /eqP->; rewrite addey ?leey.
have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last.
by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey.
apply/lee_addgt0Pr => _/posnumP[eps].
have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn.
apply: le_trans.
by apply: (@ereal_inf_lbound _ _ (edist (x, a))); exists a.
apply: le_trans; first exact: (@edist_triangle _ _ _ y).
by rewrite -addeA leeD2lE // ltW.
Qed.
by rewrite /edist_inf A0 ?image_set0 ?ereal_inf0 addey.
have [fyn|] := boolP (edist_inf y \is a fin_num); first last.
by rewrite ge0_fin_numE// ?ltey negbK => /eqP->; rewrite addey ?leey.
have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last.
by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey.
apply/lee_addgt0Pr => _/posnumP[eps].
have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn.
apply: le_trans.
by apply: (@ereal_inf_lbound _ _ (edist (x, a))); exists a.
apply: le_trans; first exact: (@edist_triangle _ _ _ y).
by rewrite -addeA leeD2lE // ltW.
Qed.
Lemma edist_inf_continuousUsed by
- mathcomp.analysis.normedtype_theory.urysohn
Source code : continuous edist_inf.
Proof.
move=> z; have [A0|/= /set0P[a0 Aa0]] := eqVneq A set0.
rewrite /edist_inf A0.
under eq_fun do rewrite image_set0 ereal_inf0.
exact: cvg_cst.
have [] := eqVneq (edist_inf z) +oo%E.
move=> /[dup] fzp /ereal_inf_pinfty => zAp U /= Ufz.
have : nbhs z (ball z 1) by exact: nbhsx_ballx.
apply: filter_app; near_simpl; near=> w => bz1w.
suff /= -> : (edist_inf w) = +oo%E by apply: nbhs_singleton; rewrite -fzp.
apply/ereal_inf_pinfty => r [a Aa] war; apply/zAp; exists a => //.
have /gee0P[|[r' r'pos war']] := edist_ge0 (w, a).
by rewrite war => ->; apply: zAp; exists a.
have := @edist_triangle _ _ z w a; rewrite war'; apply: contra_leP => _.
rewrite (@le_lt_trans _ _ (1 + r'%:E)%E) ?leeD2r ?edist_fin//.
by rewrite -EFinD [edist (z, a)]zAp ?ltey //; exists a.
rewrite -ltey -ge0_fin_numE ?edist_inf_ge0 // => fz_fin.
rewrite /continuous_at -[edist_inf z]fineK //; apply/fine_cvgP.
have fwfin : \forall wSource code \near z, edist_inf w \is a fin_num.
(have : nbhs z (ball z 1) by exact: nbhsx_ballx); apply: filter_app.
near=> t => bz1; rewrite ge0_fin_numE ?edist_inf_ge0 //.
rewrite (le_lt_trans (edist_inf_triangle _ z))//.
rewrite -ge0_fin_numE ?adde_ge0 ?edist_inf_ge0 //.
rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //.
exact/ball_sym.
split => //; apply/(@metricType_numDomainType.cvgrPdist_le _ R^o) => _/posnumP[eps].
have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx.
apply: filter_app; near_simpl; move: fwfin; apply: filter_app.
near=> t => tfin /= /[dup] ?.
have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num.
move=> /(@edist_fin _ _ _ (z, t)) - /(_ trivial).
rewrite -[edist (z, t)]fineK ?lee_fin //; apply: le_trans.
rewrite ler_norml; apply/andP; split.
rewrite lerBrDr addrC lerBlDr addrC -fineD //.
rewrite -lee_fin ?fineK // ?fin_numD ?ztfin ?fz_fin // edist_sym.
by rewrite edist_sym; exact: edist_inf_triangle.
rewrite lerBlDr -fineD // -lee_fin ?fineK // ?fin_numD ?tfin ?ztfin //.
by rewrite edist_sym; exact: edist_inf_triangle.
Unshelve. all: by end_near. Qed.
rewrite /edist_inf A0.
under eq_fun do rewrite image_set0 ereal_inf0.
exact: cvg_cst.
have [] := eqVneq (edist_inf z) +oo%E.
move=> /[dup] fzp /ereal_inf_pinfty => zAp U /= Ufz.
have : nbhs z (ball z 1) by exact: nbhsx_ballx.
apply: filter_app; near_simpl; near=> w => bz1w.
suff /= -> : (edist_inf w) = +oo%E by apply: nbhs_singleton; rewrite -fzp.
apply/ereal_inf_pinfty => r [a Aa] war; apply/zAp; exists a => //.
have /gee0P[|[r' r'pos war']] := edist_ge0 (w, a).
by rewrite war => ->; apply: zAp; exists a.
have := @edist_triangle _ _ z w a; rewrite war'; apply: contra_leP => _.
rewrite (@le_lt_trans _ _ (1 + r'%:E)%E) ?leeD2r ?edist_fin//.
by rewrite -EFinD [edist (z, a)]zAp ?ltey //; exists a.
rewrite -ltey -ge0_fin_numE ?edist_inf_ge0 // => fz_fin.
rewrite /continuous_at -[edist_inf z]fineK //; apply/fine_cvgP.
have fwfin : \forall wSource code \near z, edist_inf w \is a fin_num.
(have : nbhs z (ball z 1) by exact: nbhsx_ballx); apply: filter_app.
near=> t => bz1; rewrite ge0_fin_numE ?edist_inf_ge0 //.
rewrite (le_lt_trans (edist_inf_triangle _ z))//.
rewrite -ge0_fin_numE ?adde_ge0 ?edist_inf_ge0 //.
rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //.
exact/ball_sym.
split => //; apply/(@metricType_numDomainType.cvgrPdist_le _ R^o) => _/posnumP[eps].
have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx.
apply: filter_app; near_simpl; move: fwfin; apply: filter_app.
near=> t => tfin /= /[dup] ?.
have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num.
move=> /(@edist_fin _ _ _ (z, t)) - /(_ trivial).
rewrite -[edist (z, t)]fineK ?lee_fin //; apply: le_trans.
rewrite ler_norml; apply/andP; split.
rewrite lerBrDr addrC lerBlDr addrC -fineD //.
rewrite -lee_fin ?fineK // ?fin_numD ?ztfin ?fz_fin // edist_sym.
by rewrite edist_sym; exact: edist_inf_triangle.
rewrite lerBlDr -fineD // -lee_fin ?fineK // ?fin_numD ?tfin ?ztfin //.
by rewrite edist_sym; exact: edist_inf_triangle.
Unshelve. all: by end_near. Qed.
Lemma edist_inf0Used by
- mathcomp.analysis.normedtype_theory.urysohn
Source code aSource code : A a -> edist_inf a = 0%E.
Proof.
move=> Aa; apply: le_anti; apply/andP; split; last exact: edist_inf_ge0.
by apply: ereal_inf_lbound; exists a => //; exact: edist_refl.
Qed.
by apply: ereal_inf_lbound; exists a => //; exact: edist_refl.
Qed.
End edist_inf.
#[global]
Hint Extern 0 (is_true (0 <= edist_inf _ _)%E) =>
solve [apply: edist_inf_ge0] : core.
#[global]
Hint Extern 0 (is_true (edist_inf _ _ != -oo%E)) =>
solve [apply: edist_inf_neqNy] : core.