Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mathcomp master hausdorff close #177

Merged
merged 8 commits into from
May 6, 2020
Merged

Mathcomp master hausdorff close #177

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
27a8fc9
tentative definitions of T2separated and closeness
affeldt-aist Mar 5, 2020
5a61fa9
ported closness to topological spaces and link with hausdorff
CohenCyril Mar 9, 2020
0639e16
topological type mixin for ereal
affeldt-aist Mar 10, 2020
b085a9a
add lemmas and perform generalizations
affeldt-aist Apr 14, 2020
ef24876
fix the definition of le_ereal, lt_ereal
affeldt-aist Apr 20, 2020
5475ebe
cleanup (wip)
affeldt-aist Apr 21, 2020
827adb1
fix lee_pinfty and lee_ninfty
affeldt-aist Apr 26, 2020
7d1689b
small renamings and left a comment for later on
CohenCyril May 6, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion theories/altreals/distr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1220,7 +1220,7 @@ set c1 : R := _ / _; set c2 : R := _ / _; have eqc2: c2 = 1 - c1.
set c := (li + l j); pose z := (c * c1 * f xi + c * c2 * f (x j)).
apply/(@le_trans _ _ z); last by rewrite /z ![_*(_/_)]mulrC !mulfVK.
rewrite {}/z -![c * _ * _]mulrA -mulrDr ler_wpmul2l ?addr_ge0 //.
rewrite eqc2 cvx_f // divr_ge0 ?addr_ge0 //=.
rewrite eqc2 cvx_f // ?lee_ninfty ?lee_pinfty // divr_ge0 ?addr_ge0 //=.
by rewrite ler_pdivr_mulr ?mul1r ?ler_addl ?ltr_paddl.
Qed.
End Jensen.
Expand Down
9 changes: 5 additions & 4 deletions theories/altreals/realseq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,14 +75,14 @@ Qed.
Lemma nbh_pinfW (P : forall x, nbh x -> Prop) :
(forall M, P _ (@NPInf R M)) -> forall (v : nbh +oo), P _ v.
Proof.
move=> ih ; move: {-2}+oo (erefl (@ERPInf R)).
move=> ih; move: {-2}+oo%E (erefl (@ERPInf R)).
by move=> e eE v; case: v eE => // c' e' h [->].
Qed.

Lemma nbh_ninfW (P : forall x, nbh x -> Prop) :
(forall M, P _ (@NNInf R M)) -> forall (v : nbh -oo), P _ v.
Proof.
move=> ih ; move: {-2}-oo (erefl (@ERNInf R)).
move=> ih ; move: {-2}-oo%E (erefl (@ERNInf R)).
by move=> e eE v; case: v eE => // c' e' h [->].
Qed.
End NbhElim.
Expand Down Expand Up @@ -386,7 +386,8 @@ Lemma ncvg_gt (u : nat -> R) (l1 l2 : {ereal R}) :
exists K, forall n, (K <= n)%N -> (l1 < (u n)%:E)%E.
Proof.
case: l1 l2 => [l1||] [l2||] //=; first last.
+ by move=> _ _; exists 0%N. + by move=> _ _; exists 0%N.
+ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
+ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
+ by move=> _ /(_ (NPInf l1)) [K cv]; exists K => n /cv.
move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
Expand Down Expand Up @@ -439,7 +440,7 @@ move=> p; rewrite -[xchooseb _](ncvg_uniq cv_u_l) //.
by apply/asboolP/(xchoosebP p).
Qed.

Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo.
Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo%E.
Proof.
move=> h; rewrite /nlim; case: {-}_ / idP => // p.
by case: h; case/existsbP: p => l /asboolP; exists l.
Expand Down
5 changes: 3 additions & 2 deletions theories/altreals/realsum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -174,10 +174,11 @@ Proof.
move=> mono_u; pose E := [pred x | `[exists n, x == u n]].
have nzE: nonempty E by exists (u 0%N); apply/imsetbP; exists 0%N.
case/boolP: `[< has_sup E >] => /asboolP; last first.
move/has_supPn=> -/(_ nzE) h; exists +oo => //; elim/nbh_pinfW => M /=.
move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=.
case/(_ M): h=> x /imsetbP[K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
by apply/(lt_le_trans lt_MuK)/mono_u.
move=> supE; exists (sup E)%:E => //; elim/nbh_finW=>e /= gt0_e.
move=> supE; exists (sup E)%:E => //; first exact: lte_ninfty.
elim/nbh_finW=>e /= gt0_e.
case: (sup_adherent supE gt0_e)=> x /imsetbP[K ->] lt_uK.
exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
by apply/sup_upper_bound/imsetbP=> //; exists n.
Expand Down
78 changes: 74 additions & 4 deletions theories/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
From mathcomp Require Import ssralg matrix.
From mathcomp Require Import fintype bigop ssralg matrix.
Require Import boolp.

(******************************************************************************)
Expand Down Expand Up @@ -349,6 +349,14 @@ Qed.
Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z.
Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed.

Lemma subsetI_neq0 T (A B C D : set T) :
A `<=` B -> C `<=` D -> A `&` C !=set0 -> B `&` D !=set0.
Proof. by move=> AB CD [x [/AB Bx /CD Dx]]; exists x. Qed.

Lemma subsetI_eq0 T (A B C D : set T) :
A `<=` B -> C `<=` D -> B `&` D = set0 -> A `&` C = set0.
Proof. by move=> AB /(subsetI_neq0 AB); rewrite -!set0P => /contra_eq. Qed.

Lemma setD_eq0 A (X Y : set A) : (X `\` Y = set0) = (X `<=` Y).
Proof.
rewrite propeqE; split=> [XDY0 a|sXY].
Expand All @@ -371,14 +379,17 @@ Proof. by rewrite predeqE => ?; split=> [[]|[]]. Qed.
Lemma setIT {A} (X : set A) : X `&` setT = X.
Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma setTI {A} (X : set A) : setT `&` X = X.
Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma setI0 {A} (X : set A) : X `&` set0 = set0.
Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma set0I A (Y : set A) : set0 `&` Y = set0.
Proof. by rewrite setIC setI0. Qed.

Lemma setICl {A} (X : set A) : ~` X `&` X = set0.
Proof. by rewrite predeqE => ?; split => // -[]. Qed.
Proof. by rewrite predeqE => ?; split => // -[]. Qed.

Lemma setIA {A} (X Y Z : set A) : X `&` (Y `&` Z) = X `&` Y `&` Z.
Proof. by rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.
Expand All @@ -403,10 +414,16 @@ Lemma setUC A : commutative (@setU A).
Proof. move=> p q; rewrite /setU predeqE => a; tauto. Qed.

Lemma set0U T (X : set T) : set0 `|` X = X.
Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|right]. Qed.
Proof. by rewrite predeqE => t; split; [case|right]. Qed.

Lemma setU0 T (X : set T) : X `|` set0 = X.
Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|left]. Qed.
Proof. by rewrite predeqE => t; split; [case|left]. Qed.

Lemma setTU T (X : set T) : setT `|` X = setT.
Proof. by rewrite predeqE => t; split; [case|left]. Qed.

Lemma setUT T (X : set T) : X `|` setT = setT.
Proof. by rewrite predeqE => t; split; [case|right]. Qed.

Lemma setU_eq0 T (X Y : set T) : (X `|` Y = set0) = ((X = set0) /\ (Y = set0)).
Proof. by rewrite -!subset0 subUset. Qed.
Expand All @@ -425,6 +442,26 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
Qed.

Lemma setIDl T : left_distributive (@setI T) (@setU T).
Proof.
move=> X Y Z; rewrite predeqE => t; split.
by move=> [[Xt|Yt] Zt]; [left|right].
by move=> [[Xt Zt]|[Yt Zt]]; split => //; [left|right].
Qed.

Lemma setIDr T : right_distributive (@setI T) (@setU T).
Proof. by move=> X Y Z; rewrite ![X `&` _]setIC setIDl. Qed.

Lemma setUDl T : left_distributive (@setU T) (@setI T).
Proof.
move=> X Y Z; rewrite predeqE => t; split.
by move=> [[Xt Yt]|Zt]; split; by [left|right].
by move=> [[Xt|Zt] [Yt|Zt']]; by [left|right].
Qed.

Lemma setUDr T : right_distributive (@setU T) (@setI T).
Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.

Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
Definition is_fun {A B} (f : A -> B -> Prop) := all (is_subset1 \o f).
Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
Expand Down Expand Up @@ -476,6 +513,39 @@ Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a
is_subset1 (f a) -> forall b, f a b -> fun_of_rel f0 f a = b.
Proof. by move=> fa_prop b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.

Section SetMonoids.
Variable (T : Type).

Import Monoid.
Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
Canonical setU_comoid := ComLaw (@setUC T).
Canonical setU_mul_monoid := MulLaw (@setTU T) (@setUT T).
Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
Canonical setI_comoid := ComLaw (@setIC T).
Canonical setI_mul_monoid := MulLaw (@set0I T) (@setI0 T).
Canonical setU_add_monoid := AddLaw (@setUDl T) (@setUDr T).
Canonical setI_add_monoid := AddLaw (@setIDl T) (@setIDr T).

End SetMonoids.

Lemma bigcup_ord T n (A : nat -> set T) :
\big[setU/set0]_(i < n) A i = \bigcup_(i in [set k | (k < n)%N]) A i.
Proof.
elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE; split => -[].
rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
by move=> [A0|[i AS]]; [exists 0%N|exists i.+1].
by move=> [[|i] Ai]; [left|right; exists i].
Qed.

Lemma bigcap_ord T n (A : nat -> set T) :
\big[setI/setT]_(i < n) A i = \bigcap_(i in [set k | (k < n)%N]) A i.
Proof.
elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE.
rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
by move=> [A0 AS] [|i]// /AS.
by move=> AP; split => [|i i_lt]; apply: AP.
Qed.

Module Pointed.

Definition point_of (T : Type) := T.
Expand Down
16 changes: 8 additions & 8 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,10 +108,10 @@ Lemma diff_locallyxP (x : V) (f : V -> W) :
Proof.
split=> [dxf|[dfc dxf]].
split => //; apply: eqaddoEx => h; have /diffE -> := dxf.
rewrite lim_id addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
by congr ('o); rewrite funeqE => k /=; rewrite addrK.
apply/diffP; split=> //; apply: eqaddoEx; move=> y.
rewrite lim_id -[in LHS](subrK x y) dxf; congr (_ + _).
rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _).
rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x).
by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0.
Qed.
Expand Down Expand Up @@ -297,7 +297,7 @@ rewrite /derive => /diff_locally -> /=; set k := 'o _.
evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
rewrite funeqE=> h; rewrite !scalerDr scalerN /cst /=.
by rewrite addrC !addrA addNr add0r linearZ /= scalerA /g.
apply: cvg_map_lim.
apply: cvg_map_lim => //.
pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
Expand Down Expand Up @@ -525,7 +525,7 @@ suff /diff_locally /hdf -> : differentiable f x.
apply/diffP; apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\
forall y, f y = f (lim x) + df (y - lim x) +o_(y \near x) (y - lim x))).
exists df; split=> //; apply: eqaddoEx => z.
rewrite (hdf _ dxf) !addrA lim_id /(_ \o _) /= subrK [f _ + _]addrC addrK.
rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK.
rewrite -addrA -[LHS]addr0; congr (_ + _).
apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
Expand Down Expand Up @@ -1376,7 +1376,7 @@ Proof.
move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_right_proper_filter x.
apply: (@cvg_map_lim _ _ _ (at_right _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
by exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
Qed.

Expand All @@ -1386,7 +1386,7 @@ Proof.
move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_left_proper_filter x.
apply: (@cvg_map_lim _ _ _ (at_left _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _].
by apply: xe_A => //; rewrite eq_sym.
Qed.
Expand All @@ -1411,7 +1411,7 @@ Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
Proof.
move=> fle0 fcv; rewrite -oppr_ge0.
have limopp : - lim (f @ F) = lim (- f @ F).
by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgN.
by apply: Logic.eq_sym; apply: cvg_map_lim => //; apply: cvgN.
rewrite limopp; apply: le0r_cvg_map; last by rewrite -limopp; apply: cvgN.
by move: fle0; apply: filterS => x; rewrite oppr_ge0.
Qed.
Expand All @@ -1423,7 +1423,7 @@ Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (F
Proof.
move=> lefg fcv gcv; rewrite -subr_ge0.
have eqlim : lim (g @ F) - lim (f @ F) = lim ((g - f) @ F).
by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgD => //; apply: cvgN.
by apply/esym; apply: cvg_map_lim => //; apply: cvgD => //; apply: cvgN.
rewrite eqlim; apply: le0r_cvg_map; last first.
by rewrite /(cvg _) -eqlim /=; apply: cvgD => //; apply: cvgN.
by move: lefg; apply: filterS => x; rewrite subr_ge0.
Expand Down
58 changes: 39 additions & 19 deletions theories/ereal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,16 +29,18 @@ End ExtendedReals.
(* TODO: the following notations should have scopes. *)

(*Notation "\+inf" := (@ERPInf _).*)
Notation "+oo" := (@ERPInf _).
Notation "+oo" := (@ERPInf _) : ereal_scope.
(*Notation "\-inf" := (@ERNInf _).*)
Notation "-oo" := (@ERNInf _).
Notation "-oo" := (@ERNInf _) : ereal_scope.
Notation "x %:E" := (@ERFin _ x) (at level 2, format "x %:E").

Notation "{ 'ereal' R }" := (er R) (format "{ 'ereal' R }").

Bind Scope ereal_scope with er.
Delimit Scope ereal_scope with E.

Local Open Scope ereal_scope.

Section EqEReal.
Variable (R : eqType).

Expand All @@ -65,7 +67,7 @@ Variable (R : choiceType).

Definition code (x : {ereal R}) :=
match x with
| x%:E => GenTree.Node 0 [:: GenTree.Leaf x]
| x%:E => GenTree.Node 0 [:: GenTree.Leaf x]
| +oo => GenTree.Node 1 [::]
| -oo => GenTree.Node 2 [::]
end.
Expand Down Expand Up @@ -99,19 +101,19 @@ Implicit Types (x y : {ereal R}).

Definition le_ereal x1 x2 :=
match x1, x2 with
| -oo, _ | _, +oo => true
| +oo, _ | _, -oo => false

| -oo, x%:E | x%:E, +oo => x \is Num.real
| x1%:E, x2%:E => x1 <= x2
| -oo, _ | _, +oo => true
| +oo, _ | _, -oo => false
end.

Definition lt_ereal x1 x2 :=
match x1, x2 with
| -oo, -oo | +oo, +oo => false
| -oo, _ | _ , +oo => true
| +oo, _ | _ , -oo => false

| -oo, x%:E | x%:E, +oo => x \is Num.real
| x1%:E, x2%:E => x1 < x2
| -oo, -oo | +oo, +oo => false
| +oo, _ | _ , -oo => false
| -oo, _ => true
end.

Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.
Expand All @@ -121,10 +123,14 @@ Lemma le_refl_ereal : reflexive le_ereal.
Proof. by case => /=. Qed.

Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
Proof. by case=> [?||][?||] //= /le_anti ->. Qed.
Proof. by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.

Lemma le_trans_ereal : ssrbool.transitive le_ereal.
Proof. by case=> [?||][?||][?||] //=; exact: le_trans. Qed.
Proof.
case=> [?||][?||][?||] //=; rewrite -?comparabler0; first exact: le_trans.
by move=> /le_comparable cmp /(comparabler_trans cmp).
by move=> cmp /ge_comparable /comparabler_trans; apply.
Qed.

Fact ereal_display : unit. Proof. by []. Qed.

Expand All @@ -151,12 +157,24 @@ Notation "x < y <= z" := ((lte x y) && (lee y z)) : ereal_scope.
Notation "x <= y < z" := ((lee x y) && (lte y z)) : ereal_scope.
Notation "x < y < z" := ((lte x y) && (lte y z)) : ereal_scope.

Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y).
Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y)%O.
Proof. by []. Qed.

Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y).
Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y)%O.
Proof. by []. Qed.

Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
Proof. exact: num_real. Qed.

Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
Proof. case: x => //= r; exact: num_real. Qed.

Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
Proof. exact: num_real. Qed.

Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
Proof. case: x => //= r; exact: num_real. Qed.

Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : {ereal R}).
Expand Down Expand Up @@ -196,22 +214,24 @@ Lemma meetKU_ereal y x : max_ereal x (min_ereal x y) = x.
Proof. by case: x y => [?||][?||] //=; rewrite (meetKU, joinxx). Qed.

Lemma leEmeet_ereal x y : (x <= y)%E = (min_ereal x y == x).
Proof. by case: x y => [x||][y||] //=; [exact: leEmeet | rewrite eqxx]. Qed.
Proof.
case: x y => [x||][y||] //=; rewrite ?eqxx ?lee_pinfty ?lee_ninfty //.
exact: leEmeet.
Qed.

Lemma meetUl_ereal : left_distributive min_ereal max_ereal.
Proof.
by case=> [?||][?||][?||] //=; rewrite ?(meetUl, meetUK, meetKUC, joinxx).
Qed.

Lemma minE_ereal x y : min_ereal x y = if le_ereal x y then x else y.
Proof. by case: x y => [?||][?||] //=; case: leP. Qed.
Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: leP. Qed.

Lemma maxE_ereal x y : max_ereal x y = if le_ereal y x then x else y.
Proof.
Proof. by case: x y => [?||][?||] //=; case: ltP. Qed.
Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: ltP. Qed.

Lemma le_total_ereal : total (@le_ereal R).
Proof. by case=> [?||][?||] //=; exact: le_total. Qed.
Proof. by case=> [?||][?||] //=; rewrite ?num_real //; exact: le_total. Qed.

Definition ereal_latticeMixin :=
LatticeMixin min_erealC max_erealC min_erealA max_erealA
Expand Down
2 changes: 1 addition & 1 deletion theories/landau.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1139,7 +1139,7 @@ Hypothesis (normm_s : forall k x, `|s k x| = `|k| * `|x|).
(* - locally lipschitz => continuous at a point *)
(* - lipschitz => uniformly continous *)

Local Notation "'+oo'" := (@ERPInf R).
Local Notation "'+oo'" := (@pinfty_locally R).

Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.op s_law}) :
(f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.
Expand Down
Loading