# Compatibility with the real numbers of Coq
Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
Require Import Rtrigo1 Reals.
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope R_scope.
Lemma
Req_EM_T
(
r1
r2
: R)
: {r1 = r2} + {r1 <> r2}.
Proof.
case: (
total_order_T r1 r2)
=> [[r1Lr2 | <-] | r1Gr2].
- by right=> r1Er2; case: (
Rlt_irrefl r1)
; rewrite {2}r1Er2.
- by left.
by right=> r1Er2; case: (
Rlt_irrefl r1)
; rewrite {1}r1Er2.
Qed.
Definition
eqr
(
r1
r2
: R)
: bool :=
if Req_EM_T r1 r2 is left _ then true else false.
Lemma
eqrP
: Equality.axiom eqr.
Proof.
Canonical
R_eqMixin
:= EqMixin eqrP.
Canonical
R_eqType
:= Eval hnf in EqType R R_eqMixin.
Fact
inhR
: inhabited R.
Proof.
Definition
pickR
(
P
: pred R) (
n
: nat)
:=
let
x
:= epsilon inhR P in if P x then Some x else None.
Fact
pickR_some
P
n
x
: pickR P n = Some x -> P x.
Proof.
by rewrite /pickR; case: (
boolP (
P _))
=> // Px [<-]. Qed.
Fact
pickR_ex
(
P
: pred R)
:
(
exists
x
: R, P x)
-> exists
n,
pickR P n.
Proof.
Fact
pickR_ext
(
P
Q
: pred R)
: P =1 Q -> pickR P =1 pickR Q.
Proof.
Definition
R_choiceMixin
: choiceMixin R :=
Choice.Mixin pickR_some pickR_ex pickR_ext.
Canonical
R_choiceType
:= Eval hnf in ChoiceType R R_choiceMixin.
Fact
RplusA
: associative (
Rplus).
Proof.
Definition
R_zmodMixin
:= ZmodMixin RplusA Rplus_comm Rplus_0_l Rplus_opp_l.
Canonical
R_zmodType
:= Eval hnf in ZmodType R R_zmodMixin.
Fact
RmultA
: associative (
Rmult).
Proof.
Fact
R1_neq_0
: R1 != R0.
Proof.
by apply/eqP/R1_neq_R0. Qed.
Definition
R_ringMixin
:= RingMixin RmultA Rmult_1_l Rmult_1_r
Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.
Canonical
R_ringType
:= Eval hnf in RingType R R_ringMixin.
Canonical
R_comRingType
:= Eval hnf in ComRingType R Rmult_comm.
Import Monoid.
Canonical
Radd_monoid
:= Law RplusA Rplus_0_l Rplus_0_r.
Canonical
Radd_comoid
:= ComLaw Rplus_comm.
Canonical
Rmul_monoid
:= Law RmultA Rmult_1_l Rmult_1_r.
Canonical
Rmul_comoid
:= ComLaw Rmult_comm.
Canonical
Rmul_mul_law
:= MulLaw Rmult_0_l Rmult_0_r.
Canonical
Radd_add_law
:= AddLaw Rmult_plus_distr_r Rmult_plus_distr_l.
Definition
Rinvx
r
:= if (
r != 0)
then / r else r.
Definition
unit_R
r
:= r != 0.
Lemma
RmultRinvx
: {in unit_R, left_inverse 1 Rinvx Rmult}.
Proof.
move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_l //; apply/eqP.
Qed.
Lemma
RinvxRmult
: {in unit_R, right_inverse 1 Rinvx Rmult}.
Proof.
move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_r //; apply/eqP.
Qed.
Lemma
intro_unit_R
x
y
: y * x = 1 /\ x * y = 1 -> unit_R x.
Proof.
Lemma
Rinvx_out
: {in predC unit_R, Rinvx =1 id}.
Proof.
by move=> x; rewrite inE/= /Rinvx -if_neg => ->. Qed.
Definition
R_unitRingMixin
:=
UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.
Canonical
R_unitRing
:=
Eval hnf in UnitRingType R R_unitRingMixin.
Canonical
R_comUnitRingType
:=
Eval hnf in [comUnitRingType of R].
Lemma
R_idomainMixin
x
y
: x * y = 0 -> (
x == 0)
|| (
y == 0).
Proof.
by move=> /Rmult_integral []->; rewrite eqxx ?orbT. Qed.
Canonical
R_idomainType
:= Eval hnf in IdomainType R R_idomainMixin.
Lemma
R_fieldMixin
: GRing.Field.mixin_of [unitRingType of R].
Proof.
by done. Qed.
Definition
R_fieldIdomainMixin
:= FieldIdomainMixin R_fieldMixin.
Canonical
R_fieldType
:= FieldType R R_fieldMixin.
Reflect the order on the reals to bool
Definition
Rleb
r1
r2
:= if Rle_dec r1 r2 is left _ then true else false.
Definition
Rltb
r1
r2
:= Rleb r1 r2 && (
r1 != r2).
Definition
Rgeb
r1
r2
:= Rleb r2 r1.
Definition
Rgtb
r1
r2
:= Rltb r2 r1.
Lemma
RlebP
r1
r2
: reflect (
r1 <= r2) (
Rleb r1 r2).
Proof.
Lemma
RltbP
r1
r2
: reflect (
r1 < r2) (
Rltb r1 r2).
Proof.
rewrite /Rltb /Rleb; apply: (
iffP idP)
; case: Rle_dec=> //=.
- by case=> // r1Er2 /eqP[].
- by move=> _ r1Lr2; apply/eqP/Rlt_not_eq.
by move=> Nr1Lr2 r1Lr2; case: Nr1Lr2; left.
Qed.
Section
ssreal_struct
.
Import GRing.Theory.
Import Num.Theory.
Import Num.Def.
Local Open Scope R_scope.
Lemma
Rleb_norm_add
x
y
: Rleb (
Rabs (
x + y)) (
Rabs x + Rabs y).
Proof.
by apply/RlebP/Rabs_triang. Qed.
Lemma
addr_Rgtb0
x
y
: Rltb 0 x -> Rltb 0 y -> Rltb 0 (
x + y).
Proof.
by move/RltbP=> Hx /RltbP Hy; apply/RltbP/Rplus_lt_0_compat. Qed.
Lemma
Rnorm0_eq0
x
: Rabs x = 0 -> x = 0.
Proof.
by move=> H; case: (
x == 0)
/eqP=> // /Rabs_no_R0. Qed.
Lemma
Rleb_leVge
x
y
: Rleb 0 x -> Rleb 0 y -> (
Rleb x y)
|| (
Rleb y x).
Proof.
move/RlebP=> Hx /RlebP Hy; case: (
Rlt_le_dec x y).
by move/Rlt_le/RlebP=> ->.
by move/RlebP=> ->; rewrite orbT.
Qed.
Lemma
RnormM
: {morph Rabs :
x
y
/ x * y}.
Proof.
Lemma
Rleb_def
x
y
: (
Rleb x y)
= (
Rabs (
y - x)
== y - x).
Proof.
apply/(
sameP (
RlebP x y))
/(
iffP idP)
=> [/eqP H| /Rle_minus H].
apply: Rminus_le; rewrite -Ropp_minus_distr.
apply/Rge_le/Ropp_0_le_ge_contravar.
by rewrite -H; apply: Rabs_pos.
apply/eqP/Rabs_pos_eq.
rewrite -Ropp_minus_distr.
by apply/Ropp_0_ge_le_contravar/Rle_ge.
Qed.
Lemma
Rltb_def
x
y
: (
Rltb x y)
= (
y != x)
&& (
Rleb x y).
Proof.
Definition
R_numMixin
:= NumMixin Rleb_norm_add addr_Rgtb0 Rnorm0_eq0
Rleb_leVge RnormM Rleb_def Rltb_def.
Canonical
R_porderType
:= POrderType ring_display R R_numMixin.
Canonical
R_numDomainType
:= NumDomainType R R_numMixin.
Canonical
R_normedZmodType
:= NormedZmodType R R R_numMixin.
Lemma
RleP
: forall
x
y,
reflect (
Rle x y) (
x <= y)
%R.
Proof.
Lemma
RltP
: forall
x
y,
reflect (
Rlt x y) (
x < y)
%R.
Proof.
Canonical
R_numFieldType
:= [numFieldType of R].
Lemma
Rreal_axiom
(
x
: R)
: (
0 <= x)
%R || (
x <= 0)
%R.
Proof.
case: (
Rle_dec 0 x)
=> [/RleP ->|] //.
by move/Rnot_le_lt/Rlt_le/RleP=> ->; rewrite orbT.
Qed.
Lemma
R_total
: totalPOrderMixin R_porderType.
Proof.
move=> x y; case: (
Rle_lt_dec x y)
=> [/RleP -> //|/Rlt_le/RleP ->];
by rewrite orbT.
Qed.
Canonical
R_latticeType
:= LatticeType R R_total.
Canonical
R_distrLatticeType
:= DistrLatticeType R R_total.
Canonical
R_orderType
:= OrderType R R_total.
Canonical
R_realDomainType
:= [realDomainType of R].
Canonical
R_realFieldType
:= [realFieldType of R].
Lemma
Rarchimedean_axiom
: Num.archimedean_axiom R_numDomainType.
Proof.
Canonical
R_realArchiFieldType
:= ArchiFieldType R Rarchimedean_axiom.
Here are the lemmas that we will use to prove that R has
the rcfType structure.
Lemma
continuity_eq
f
g
: f =1 g -> continuity f -> continuity g.
Proof.
move=> Hfg Hf x eps Heps.
have [y [Hy1 Hy2]]:= Hf x eps Heps.
by exists y; split=> // z; rewrite -!Hfg; exact: Hy2.
Qed.
Lemma
continuity_sum
(
I
: finType)
F
(
P
: pred I)
:
(
forall
i,
P i -> continuity (
F i))
->
continuity (
fun
x
=> (
\sum_(
i
| P i) ((
F i)
x)))
%R.
Proof.
Lemma
continuity_exp
f
n:
continuity f -> continuity (
fun
x
=> (
f x)
^+ n)
%R.
Proof.
Lemma
Rreal_closed_axiom
: Num.real_closed_axiom R_numDomainType.
Proof.
move=> p a b; rewrite !le_eqVlt.
case Hpa: ((
p.
[a])
%R == 0%R).
by move=> ? _ ; exists a=> //; rewrite lexx le_eqVlt.
case Hpb: ((
p.
[b])
%R == 0%R).
by move=> ? _; exists b=> //; rewrite lexx le_eqVlt andbT.
case Hab: (
a == b).
by move=> _; rewrite (
eqP Hab)
eq_sym Hpb (
ltNge 0)
/=; case/andP=> /ltW ->.
rewrite eq_sym Hpb /=; clear=> /RltbP Hab /andP [] /RltbP Hpa /RltbP Hpb.
suff Hcp: continuity (
fun
x
=> (
p.
[x])
%R).
have [z [[Hza Hzb] /eqP Hz2]]:= IVT _ a b Hcp Hab Hpa Hpb.
by exists z=> //; apply/andP; split; apply/RlebP.
rewrite -[p]coefK poly_def.
set f := fun _ => _.
have Hf: (
fun (
x
: R)
=> \sum_(
i
< size p) (
p`_i * x^+i))
%R =1 f.
move=> x; rewrite /f horner_sum.
by apply: eq_bigr=> i _; rewrite hornerZ hornerXn.
apply: (
continuity_eq Hf)
; apply: continuity_sum=> i _.
apply:continuity_scal; apply: continuity_exp=> x esp Hesp.
by exists esp; split=> // y [].
Qed.
Canonical
R_rcfType
:= RcfType R Rreal_closed_axiom.
End ssreal_struct.
Local Open Scope ring_scope.
From mathcomp Require Import boolp classical_sets.
Require Import reals.
Section
ssreal_struct_contd
.
Implicit Type E : set R.
Lemma
is_upper_boundE
E
x
: is_upper_bound E x = (
ubound E)
x.
Proof.
rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
by apply/ubP => y Ey; apply/RleP/h.
Qed.
Lemma
boundE
E
: bound E = has_ubound E.
Proof.
Lemma
Rcondcomplete
E
: has_sup E -> {m | isLub E m}.
Proof.
move=> [E0 uE]; have := completeness E; rewrite boundE => /(
_ uE E0)
[x [E1 E2]].
exists x; split; first by rewrite -is_upper_boundE; apply: E1.
by move=> y; rewrite -is_upper_boundE => /E2/RleP.
Qed.
Lemma
Rsupremums_neq0
E
: has_sup E -> (
supremums E !=set0)
%classic.
Proof.
by move=> /Rcondcomplete[x [? ?]]; exists x. Qed.
Lemma
Rsup_isLub
x0
E
: has_sup E -> isLub E (
supremum x0 E).
Proof.
Lemma
real_sup_adherent
x0
E
(
eps
: R)
: (
0 < eps)
->
has_sup E -> exists2
e,
E e & (
supremum x0 E - eps)
< e.
Proof.
Lemma
Rsup_ub
x0
E
: has_sup E -> (
ubound E) (
supremum x0 E).
Proof.
by move=> supE x Ex; apply/ge_supremum_Nmem => //; exact: Rsupremums_neq0.
Qed.
Definition
real_realMixin
: Real.mixin_of _ :=
RealMixin (
@Rsup_ub (
0 : R)) (
real_sup_adherent 0).
Canonical
real_realType
:= RealType R real_realMixin.
Implicit Types (
x y : R) (
m n : nat).
Lemma
expR0
: exp (
0 : R)
= 1.
Proof.
Lemma
expRD
x
y
: exp x * exp y = exp (
x + y).
Proof.
Lemma
expRX
x
n
: exp x ^+ n = exp (
x *+ n).
Proof.
Lemma
sinD
x
y
: sin (
x + y)
= sin x * cos y + cos x * sin y.
Proof.
Lemma
cosD
x
y
: cos (
x + y)
= (
cos x * cos y - sin x * sin y).
Proof.
Lemma
RplusE
x
y
: Rplus x y = x + y
Proof.
by []. Qed.
Lemma
RminusE
x
y
: Rminus x y = x - y
Proof.
by []. Qed.
Lemma
RmultE
x
y
: Rmult x y = x * y
Proof.
by []. Qed.
Lemma
RoppE
x
: Ropp x = - x
Proof.
by []. Qed.
Lemma
RinvE
x
: x != 0 -> Rinv x = x^-1.
Proof.
by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed.
Lemma
RdivE
x
y
: y != 0 -> Rdiv x y = x / y.
Proof.
by move=> y_neq0; rewrite /Rdiv RinvE. Qed.
Lemma
INRE
n
: INR n = n%:R.
Proof.
Lemma
RsqrtE
x
: 0 <= x -> sqrt x = Num.sqrt x.
Proof.
Lemma
RpowE
x
n
: pow x n = x ^+ n.
Proof.
by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.
Lemma
RmaxE
x
y
: Rmax x y = Num.max x y.
Proof.
Lemma
RminE
x
y
: Rmin x y = Num.min x y.
Proof.
Section
bigmaxr
.
Context {R : realDomainType}.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Definition
bigmaxr
(
r
: R)
s
:= \big[Num.
max/head r s]_(
i
<- s)
i.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_nil
(
x0
: R)
: bigmaxr x0 [::] = x0.
Proof.
by rewrite /bigmaxr /= big_nil. Qed.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_un
(
x0
x
: R)
: bigmaxr x0 [:: x] = x.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxrE
(
r
: R)
s
: bigmaxr r s = foldr Num.max (
head r s) (
behead s).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigrmax_dflt
(
x
y
: R)
s
: Num.max x (
\big[Num.
max/x]_(
j
<- y :: s)
j)
=
Num.max x (
\big[Num.
max/y]_(
i
<- y :: s)
i).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_cons
(
x0
x
y
: R)
lr
:
bigmaxr x0 (
x :: y :: lr)
= Num.max x (
bigmaxr x0 (
y :: lr)).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_ler
(
x0
: R)
s
i
:
(
i < size s)
%N -> (
nth x0 s i)
<= (
bigmaxr x0 s).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_addr
(
x0
: R)
lr
(
x
: R)
:
bigmaxr (
x0 + x) (
map (
fun
y
: R => y + x)
lr)
= (
bigmaxr x0 lr)
+ x.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_mem
(
x0
: R)
lr
: (
0 < size lr)
%N -> bigmaxr x0 lr \in lr.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_mulr
(
A
: finType) (
s
: seq A) (
k
: R) (
x
: A -> R)
:
0 <= k -> bigmaxr 0 (
map (
fun
i
=> k * x i)
s)
= k * bigmaxr 0 (
map x s).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_index
(
x0
: R)
lr
:
(
0 < size lr)
%N -> (
index (
bigmaxr x0 lr)
lr < size lr)
%N.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_lerP
(
x0
: R)
lr
(
x
: R)
:
(
0 < size lr)
%N ->
reflect (
forall
i,
(
i < size lr)
%N -> (
nth x0 lr i)
<= x) ((
bigmaxr x0 lr)
<= x).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_ltrP
(
x0
: R)
lr
(
x
: R)
:
(
0 < size lr)
%N ->
reflect (
forall
i,
(
i < size lr)
%N -> (
nth x0 lr i)
< x) ((
bigmaxr x0 lr)
< x).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxrP
(
x0
: R)
lr
(
x
: R)
:
(
x \in lr /\ forall
i,
(
i < size lr)
%N -> (
nth x0 lr i)
<= x)
-> (
bigmaxr x0 lr = x).
Proof.
move=> [] /(
nthP x0)
[] j j_size j_nth x_ler; apply: le_anti; apply/andP; split.
by apply/bigmaxr_lerP => //; apply: (
leq_trans _ j_size).
by rewrite -j_nth (
bigmaxr_ler _ j_size).
Qed.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bigmaxr_lerif
(
x0
: R)
lr
:
uniq lr -> forall
i,
(
i < size lr)
%N ->
(
nth x0 lr i)
<= (
bigmaxr x0 lr)
?= iff (
i == index (
bigmaxr x0 lr)
lr).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Definition
bmaxrf
n
(
f
: {ffun 'I_n.
+1 -> R})
:=
bigmaxr (
f ord0) (
codom f).
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bmaxrf_ler
n
(
f
: {ffun 'I_n.
+1 -> R})
i
:
(
f i)
<= (
bmaxrf f).
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bmaxrf_index
n
(
f
: {ffun 'I_n.
+1 -> R})
:
(
index (
bmaxrf f) (
codom f)
< n.
+1)
%N.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Definition
index_bmaxrf
n
f
:= Ordinal (
@bmaxrf_index n f).
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
ordnat
i
n
(
ord_i
: (
i < n)
%N)
: i = Ordinal ord_i :> nat.
Proof.
by []. Qed.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
eq_index_bmaxrf
n
(
f
: {ffun 'I_n.
+1 -> R})
:
f (
index_bmaxrf f)
= bmaxrf f.
Proof.
#[deprecated(
note="To be removed. Use topology.v's bigmax/min lemmas instead.")
]
Lemma
bmaxrf_lerif
n
(
f
: {ffun 'I_n.
+1 -> R})
:
injective f -> forall
i,
(
f i)
<= (
bmaxrf f)
?= iff (
i == index_bmaxrf f).
Proof.
End bigmaxr.
End ssreal_struct_contd.
Require Import signed topology.
Section
analysis_struct
.
Canonical
R_pointedType
:= [pointedType of R for pointed_of_zmodule R_ringType].
Canonical
R_filteredType
:=
[filteredType R of R for filtered_of_normedZmod R_normedZmodType].
Canonical
R_topologicalType
: topologicalType := TopologicalType R
(
topologyOfEntourageMixin
(
uniformityOfBallMixin
(
@nbhs_ball_normE _ R_normedZmodType)
(
pseudoMetric_of_normedDomain R_normedZmodType))).
Canonical
R_uniformType
: uniformType :=
UniformType R
(
uniformityOfBallMixin (
@nbhs_ball_normE _ R_normedZmodType)
(
pseudoMetric_of_normedDomain R_normedZmodType)).
Canonical
R_pseudoMetricType
: pseudoMetricType R_numDomainType :=
PseudoMetricType R (
pseudoMetric_of_normedDomain R_normedZmodType).
Lemma
continuity_pt_nbhs
(
f
: R -> R)
x
:
continuity_pt f x <->
forall
eps
: {posnum R}, nbhs x (
fun
u
=> `|f u - f x| < eps%:num).
Proof.
split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
have [_/posnumP[d] xd_fxe] := fcont e.
exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num].
by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
have /RltP egt0 := [gt0 of e%:num].
have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
exists d%:num => //= y xyd; case: (
eqVneq x y)
=> [->|xney].
by rewrite subrr normr0.
apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
by have /RltP := xyd; rewrite distrC.
Qed.
Lemma
continuity_pt_cvg
(
f
: R -> R) (
x
: R)
:
continuity_pt f x <-> {for x, continuous f}.
Proof.
eapply iff_trans; first exact: continuity_pt_nbhs.
apply iff_sym.
have FF : Filter (
f @ x).
by typeclasses eauto.
case: (
@fcvg_ballP _ _ (
f @ x)
FF (
f x))
=> {FF}H1 H2.
split => [{H2} - /H1 {}H1 eps|{H1} H].
- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
exists x0%:num => //= Hx0' /Hx0 /=.
by rewrite /= distrC; apply.
- apply H2 => _ /posnumP[eps]; move: (
H eps)
=> {H} [_ /posnumP[x0] Hx0].
exists x0%:num => //= y /Hx0 /= {}Hx0.
by rewrite /ball /= distrC.
Qed.
Lemma
continuity_ptE
(
f
: R -> R) (
x
: R)
:
continuity_pt f x <-> {for x, continuous f}.
Proof.
Local Open Scope classical_set_scope.
Lemma
continuity_pt_cvg'
f
x
:
continuity_pt f x <-> f @ x^' --> f x.
Proof.
Lemma
continuity_pt_dnbhs
f
x
:
continuity_pt f x <->
forall
eps,
0 < eps -> x^' (
fun
u
=> `|f x - f u| < eps).
Proof.
Lemma
nbhs_pt_comp
(
P
: R -> Prop) (
f
: R -> R) (
x
: R)
:
nbhs (
f x)
P -> continuity_pt f x -> \near
x,
P (
f x).
Proof.
by move=> Lf /continuity_pt_cvg; apply. Qed.
End analysis_struct.