From 8da770d1defa55a47d5584b9f94e36f5483aedab Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 14 Mar 2023 10:12:12 +0900 Subject: [PATCH 1/4] fixes naming of topology.v - fixes #866 - fixes #867 - fixes #868 --- CHANGELOG_UNRELEASED.md | 14 ++++++ theories/topology.v | 103 +++++++++++++++++++++------------------- 2 files changed, 68 insertions(+), 49 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5c7f246c1..bfb5bf0d8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,6 +23,20 @@ + `ErealGenOInfty.measurable_set1_pinfty` -> `ErealGenOInfty.measurable_set1y` + `ErealGenCInfty.measurable_set1_ninfty` -> `ErealGenCInfty.measurable_set1Ny` + `ErealGenCInfty.measurable_set1_pinfty` -> `ErealGenCInfty.measurable_set1y` +- in `topology.v`: + + `Topological.ax1` -> `Topological.nbhs_pfilter` + + `Topological.ax2` -> `Topological.nbhsE` + + `Topological.ax3` -> `Topological.openE` + + `entourage_filter` -> `entourage_pfilter` + + `Uniform.ax1` -> `Uniform.entourage_filter` + + `Uniform.ax2` -> `Uniform.entourage_refl` + + `Uniform.ax3` -> `Uniform.entourage_inv` + + `Uniform.ax4` -> `Uniform.entourage_split_ex` + + `Uniform.ax5` -> `Uniform.nbhsE` + + `PseudoMetric.ax1` -> `PseudoMetric.ball_center` + + `PseudoMetric.ax2` -> `PseudoMetric.ball_sym` + + `PseudoMetric.ax3` -> `PseudoMetric.ball_triangle` + + `PseudoMetric.ax4` -> `PseudoMetric.entourageE` ### Generalized diff --git a/theories/topology.v b/theories/topology.v index 7be480d51..70cd51c68 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1613,10 +1613,10 @@ Module Topological. Record mixin_of (T : Type) (nbhs : T -> set (set T)) := Mixin { open : set (set T) ; - ax1 : forall p : T, ProperFilter (nbhs p) ; - ax2 : forall p : T, nbhs p = + nbhs_pfilter : forall p : T, ProperFilter (nbhs p) ; + nbhsE : forall p : T, nbhs p = [set A : set T | exists B : set T, [/\ open B, B p & B `<=` A] ] ; - ax3 : open = [set A : set T | A `<=` nbhs^~ A ] + openE : open = [set A : set T | A `<=` nbhs^~ A ] }. Record class_of (T : Type) := Class { @@ -1685,7 +1685,7 @@ Definition open := Topological.open (Topological.class T). Definition open_nbhs (p : T) (A : set T) := open A /\ A p. Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p). -Proof. by apply: Topological.ax1; case: T p => ? []. Qed. +Proof. by apply: Topological.nbhs_pfilter; case: T p => ? []. Qed. Typeclasses Opaque nbhs. Lemma nbhs_filter (p : T) : Filter (nbhs p). @@ -1697,7 +1697,7 @@ Lemma nbhsE (p : T) : nbhs p = [set A : set T | exists2 B : set T, open_nbhs p B & B `<=` A]. Proof. have -> : nbhs p = [set A : set T | exists B, [/\ open B, B p & B `<=` A] ]. - exact: Topological.ax2. + exact: Topological.nbhsE. by rewrite predeqE => A; split=> [[B [?]]|[B[]]]; exists B. Qed. @@ -1717,7 +1717,7 @@ by move=> p; rewrite /interior nbhsE => -[? [? ?]]; apply. Qed. Lemma openE : open = [set A : set T | A `<=` A^°]. -Proof. exact: Topological.ax3. Qed. +Proof. exact: Topological.openE. Qed. Lemma nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p. Proof. by rewrite nbhsE => - [? [_ ?]]; apply. Qed. @@ -3762,7 +3762,7 @@ move=> A /gcvg; rewrite nbhs_simpl; case=> N _ An. exists (g N); split => //; last by apply: An; rewrite /= ?leqnn //. apply/eqP => M; suff: g N N != f N by rewrite M; move/eqP. rewrite /g ltnn /derange eq_sym; case: (eqVneq (f N) (distincts N).1) => //. -by move=> ->; have := projT2 (sigW (npts N)). +by move=> ->; have := projT2 (sigW (npts N)). Qed. End perfect_sets. @@ -3785,11 +3785,12 @@ Module Uniform. Record mixin_of (M : Type) (nbhs : M -> set (set M)) := Mixin { entourage : (M * M -> Prop) -> Prop ; - ax1 : Filter entourage ; - ax2 : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A ; - ax3 : forall A, entourage A -> entourage (A^-1)%classic ; - ax4 : forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A ; - ax5 : nbhs = nbhs_ entourage + entourage_filter : Filter entourage ; + entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A ; + entourage_inv : forall A, entourage A -> entourage (A^-1)%classic ; + entourage_split_ex : + forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A ; + nbhsE : nbhs = nbhs_ entourage }. Record class_of (M : Type) := Class { @@ -3859,20 +3860,20 @@ Program Definition topologyOfEntourageMixin (T : Type) Topological.mixin_of nbhs := topologyOfFilterMixin _ _ _. Next Obligation. move=> T nbhsT m p. -rewrite (Uniform.ax5 m) nbhs_E; apply filter_from_proper; last first. - by move=> A entA; exists p; apply: Uniform.ax2 entA _ _. +rewrite (Uniform.nbhsE m) nbhs_E; apply filter_from_proper; last first. + by move=> A entA; exists p; apply: Uniform.entourage_refl entA _ _. apply: filter_from_filter. - by exists setT; apply: @filterT (Uniform.ax1 m). + by exists setT; apply: @filterT (Uniform.entourage_filter m). move=> A B entA entB; exists (A `&` B) => //. -exact: (@filterI _ _ (Uniform.ax1 m)). +exact: (@filterI _ _ (Uniform.entourage_filter m)). Qed. Next Obligation. -move=> T nbhsT m p A; rewrite (Uniform.ax5 m) nbhs_E => - [B entB sBpA]. -by apply: sBpA; apply: Uniform.ax2 entB _ _. +move=> T nbhsT m p A; rewrite (Uniform.nbhsE m) nbhs_E => - [B entB sBpA]. +by apply: sBpA; apply: Uniform.entourage_refl entB _ _. Qed. Next Obligation. -move=> T nbhsT m p A; rewrite (Uniform.ax5 m) nbhs_E => - [B entB sBpA]. -have /Uniform.ax4 [C entC sC2B] := entB. +move=> T nbhsT m p A; rewrite (Uniform.nbhsE m) nbhs_E => - [B entB sBpA]. +have /Uniform.entourage_split_ex [C entC sC2B] := entB. exists C => // q Cpq; rewrite nbhs_E; exists C => // r Cqr. by apply/sBpA/sC2B; exists q. Qed. @@ -3904,13 +3905,12 @@ Proof. by rewrite nbhs_simpl. Qed. Section uniformType1. Context {M : uniformType}. -Lemma entourage_refl (A : set (M * M)) x : - entourage A -> A (x, x). -Proof. by move=> entA; apply: Uniform.ax2 entA _ _. Qed. +Lemma entourage_refl (A : set (M * M)) x : entourage A -> A (x, x). +Proof. by move=> entA; apply: Uniform.entourage_refl entA _ _. Qed. -Global Instance entourage_filter : ProperFilter (@entourage M). +Global Instance entourage_pfilter : ProperFilter (@entourage M). Proof. -apply Build_ProperFilter; last exact: Uniform.ax1. +apply: Build_ProperFilter; last exact: Uniform.entourage_filter. by move=> A entA; exists (point, point); apply: entourage_refl. Qed. @@ -3918,11 +3918,11 @@ Lemma entourageT : entourage [set: M * M]. Proof. exact: filterT. Qed. Lemma entourage_inv (A : set (M * M)) : entourage A -> entourage (A^-1)%classic. -Proof. exact: Uniform.ax3. Qed. +Proof. exact: Uniform.entourage_inv. Qed. Lemma entourage_split_ex (A : set (M * M)) : entourage A -> exists2 B, entourage B & B \; B `<=` A. -Proof. exact: Uniform.ax4. Qed. +Proof. exact: Uniform.entourage_split_ex. Qed. Definition split_ent (A : set (M * M)) := get (entourage `&` [set B | B \; B `<=` A]). @@ -4084,10 +4084,10 @@ Qed. Lemma prod_ent_filter : Filter prod_ent. Proof. -have prodF := filter_prod_filter (@entourage_filter U) (@entourage_filter V). +have prodF := filter_prod_filter (@entourage_pfilter U) (@entourage_pfilter V). split; rewrite /prod_ent; last 1 first. - by move=> A B sAB /=; apply: filterS => ? [xy /sAB ??]; exists xy. -- rewrite -setMTT; apply: prod_entP filterT filterT. +- by rewrite -setMTT; apply: prod_entP filterT filterT. move=> A B /= entA entB; apply: filterS (filterI entA entB) => xy []. move=> [zt Azt ztexy] [zt' Bzt' zt'exy]; exists zt => //; split=> //. move/eqP: ztexy; rewrite -zt'exy !xpair_eqE. @@ -4539,12 +4539,14 @@ End product_uniform. Module PseudoMetric. -Record mixin_of (R : numDomainType) (M : Type) (entourage : set (set (M * M))) := Mixin { +Record mixin_of (R : numDomainType) (M : Type) + (entourage : set (set (M * M))) := Mixin { ball : M -> R -> M -> Prop ; - ax1 : forall x (e : R), 0 < e -> ball x e x ; - ax2 : forall x y (e : R), ball x e y -> ball y e x ; - ax3 : forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z; - ax4 : entourage = entourage_ ball + ball_center : forall x (e : R), 0 < e -> ball x e x ; + ball_sym : forall x y (e : R), ball x e y -> ball y e x ; + ball_triangle : + forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z; + entourageE : entourage = entourage_ ball }. Record class_of (R : numDomainType) (M : Type) := Class { @@ -4612,15 +4614,16 @@ Export PseudoMetric.Exports. Section PseudoMetricUniformity. -Lemma my_ball_le (R : numDomainType) (M : Type) (ent : set (set (M * M))) (m : PseudoMetric.mixin_of R ent) : +Lemma my_ball_le (R : numDomainType) (M : Type) (ent : set (set (M * M))) + (m : PseudoMetric.mixin_of R ent) : forall (x : M), {homo PseudoMetric.ball m x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}. Proof. move=> x e1 e2 le12 y xe1_y. move: le12; rewrite le_eqVlt => /orP [/eqP <- //|]. rewrite -subr_gt0 => lt12. -rewrite -[e2](subrK e1); apply: PseudoMetric.ax3 xe1_y. +rewrite -[e2](subrK e1); apply: PseudoMetric.ball_triangle xe1_y. suff : PseudoMetric.ball m x (PosNum lt12)%:num x by []. -exact: PseudoMetric.ax1. +exact: PseudoMetric.ball_center. Qed. Program Definition uniformityOfBallMixin (R : numFieldType) (T : Type) @@ -4628,35 +4631,37 @@ Program Definition uniformityOfBallMixin (R : numFieldType) (T : Type) (m : PseudoMetric.mixin_of R ent) : Uniform.mixin_of nbhs := UniformMixin _ _ _ _ nbhsE. Next Obligation. -move=> R T ent nbhs nbhsE m; rewrite (PseudoMetric.ax4 m). +move=> R T ent nbhs nbhsE m; rewrite (PseudoMetric.entourageE m). apply: filter_from_filter; first by exists 1 => /=. move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=. by rewrite subsetI; split=> ?; apply: my_ball_le; rewrite -leEsub// le_minl lexx ?orbT. Qed. Next Obligation. -move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m). +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.entourageE m). move=> [e egt0 sbeA] xy xey. -apply: sbeA; rewrite /= xey; exact: PseudoMetric.ax1. +by apply: sbeA; rewrite /= xey; exact: PseudoMetric.ball_center. Qed. Next Obligation. -move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m) => - [e egt0 sbeA]. -by exists e => // xy xye; apply: sbeA; apply: PseudoMetric.ax2. +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.entourageE m) => - [e egt0 sbeA]. +by exists e => // xy xye; apply: sbeA; apply: PseudoMetric.ball_sym. Qed. Next Obligation. -move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.ax4 m). +move=> R T ent nbhs nbhsE m A; rewrite (PseudoMetric.entourageE m). move=> [_/posnumP[e] sbeA]. exists [set xy | PseudoMetric.ball m xy.1 (e%:num / 2) xy.2]. by exists (e%:num / 2) => /=. move=> xy [z xzhe zyhe]; apply: sbeA. -by rewrite [e%:num]splitr; apply: PseudoMetric.ax3 zyhe. +by rewrite [e%:num]splitr; apply: PseudoMetric.ball_triangle zyhe. Qed. End PseudoMetricUniformity. -Definition ball {R : numDomainType} {M : pseudoMetricType R} := PseudoMetric.ball (PseudoMetric.class M). +Definition ball {R : numDomainType} {M : pseudoMetricType R} := + PseudoMetric.ball (PseudoMetric.class M). -Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} : entourage_ (@ball R M) = entourage. +Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} + : entourage_ (@ball R M) = entourage. Proof. by case: M=> [?[?[]]]. Qed. Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} : @@ -4697,7 +4702,7 @@ Proof. by rewrite nbhs_simpl. Qed. Lemma ball_center {R : numDomainType} (M : pseudoMetricType R) (x : M) (e : {posnum R}) : ball x e%:num x. -Proof. exact: PseudoMetric.ax1. Qed. +Proof. exact: PseudoMetric.ball_center. Qed. #[global] Hint Resolve ball_center : core. Section pseudoMetricType_numDomainType. @@ -4707,11 +4712,11 @@ Lemma ballxx (x : M) (e : R) : 0 < e -> ball x e x. Proof. by move=> e_gt0; apply: ball_center (PosNum e_gt0). Qed. Lemma ball_sym (x y : M) (e : R) : ball x e y -> ball y e x. -Proof. exact: PseudoMetric.ax2. Qed. +Proof. exact: PseudoMetric.ball_sym. Qed. Lemma ball_triangle (y x z : M) (e1 e2 : R) : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. -Proof. exact: PseudoMetric.ax3. Qed. +Proof. exact: PseudoMetric.ball_triangle. Qed. Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num). Proof. by apply/nbhs_ballP; exists eps%:num => /=. Qed. From 71a9e5ab614093035f6789241a32fbb6c6aef033 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 14 Mar 2023 11:36:56 +0900 Subject: [PATCH 2/4] fixes #865 --- classical/functions.v | 70 +++++++++++++++++++++---------------------- theories/realfun.v | 2 +- 2 files changed, 36 insertions(+), 36 deletions(-) diff --git a/classical/functions.v b/classical/functions.v index 2931ea4c1..05ad2f8f1 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -222,10 +222,10 @@ Definition set_inj := {in A &, injective f}. Definition set_bij := [/\ set_fun, set_inj & set_surj]. End MainProperties. -HB.mixin Record IsFun {aT rT} (A : set aT) (B : set rT) (f : aT -> rT) := +HB.mixin Record isFun {aT rT} (A : set aT) (B : set rT) (f : aT -> rT) := { funS : set_fun A B f }. HB.structure Definition Fun {aT rT} (A : set aT) (B : set rT) := - { f of IsFun _ _ A B f }. + { f of isFun _ _ A B f }. Notation "{ 'fun' A >-> B }" := (@Fun.type _ _ A B) : form_scope. Notation "[ 'fun' 'of' f ]" := [the {fun _ >-> _} of f : _ -> _] : form_scope. @@ -239,7 +239,7 @@ Definition phant_oinv aT rT (f : {oinv aT >-> rT}) Notation "''oinv_' f" := (@phant_oinv _ _ _ (Phantom (_ -> _) f%FUN)). HB.structure Definition OInvFun aT rT A B := - {f of OInv aT rT f & IsFun aT rT A B f}. + {f of OInv aT rT f & isFun aT rT A B f}. Notation "{ 'oinvfun' A >-> B }" := (@OInvFun.type _ _ A B) : type_scope. Notation "[ 'oinvfun' 'of' f ]" := [the {oinvfun _ >-> _} of f : _ -> _] : form_scope. @@ -264,7 +264,7 @@ Notation "f ^-1" := (@inv _ _ f%function) (only printing) : function_scope. Notation "f ^-1" := (@phant_inv _ _ _ (Phantom (_ -> _) f%FUN)) : fun_scope. Notation "f ^-1" := (@phant_inv _ _ _ (Phantom (_ -> _) f%function)) : function_scope. -HB.structure Definition InvFun aT rT A B := {f of Inv aT rT f & IsFun aT rT A B f}. +HB.structure Definition InvFun aT rT A B := {f of Inv aT rT f & isFun aT rT A B f}. Notation "{ 'invfun' A >-> B }" := (@InvFun.type _ _ A B) : type_scope. Notation "[ 'invfun' 'of' f ]" := [the {invfun _ >-> _} of f : _ -> _] : form_scope. @@ -329,7 +329,7 @@ Notation "[ 'splitinj' 'of' f ]" := [the {splitinj _ >-> _} of f : _ -> _] : form_scope. HB.structure Definition SplitInjFun aT rT (A : set aT) (B : set rT) := - {f of @SplitInj _ rT A f & @IsFun _ _ A B f}. + {f of @SplitInj _ rT A f & @isFun _ _ A B f}. Notation "{ 'splitinjfun' A >-> B }" := (@SplitInjFun.type _ _ A B) : type_scope. Notation "[ 'splitinjfun' 'of' f ]" := [the {splitinjfun _ >-> _} of f : _ -> _] : form_scope. @@ -483,7 +483,7 @@ Lemma funP {aT rT} {A : set aT} {B : set rT} (f g : {fun A >-> B}) : Proof. case: f g => [f [[ffun]]] [g [[gfun]]]/=; split=> [[->//]|/funext eqfg]. rewrite eqfg in ffun *; congr {| Fun.sort := _; Fun.class := {| - Fun.functions_IsFun_mixin := {|IsFun.funS := _|}|}|}. + Fun.functions_isFun_mixin := {|isFun.funS := _|}|}|}. exact: Prop_irrelevance. Qed. @@ -527,7 +527,7 @@ Lemma oinvV {f : {oinv aT >-> rT}} : 'oinv_('oinv_f) = omap f. Proof. by []. Qed. HB.instance Definition _ (f : {surj A >-> B}) := - IsFun.Build rT (option aT) B (some @` A) 'oinv_f oinvS. + isFun.Build rT (option aT) B (some @` A) 'oinv_f oinvS. Lemma surjoinv_inj_subproof (f : {surj A >-> B}) : OInv_Can _ _ B 'oinv_f. Proof. @@ -557,7 +557,7 @@ HB.instance Definition _ (f : {inv aT >-> rT}) := Inversible.copy inv f^-1. Lemma invV (f : {inv aT >-> rT}) : f^-1^-1 = f. Proof. by []. Qed. HB.instance Definition _ (f : {splitsurj A >-> B}) := - IsFun.Build rT aT B A f^-1 invS. + isFun.Build rT aT B A f^-1 invS. HB.instance Definition _ (f : {splitsurj A >-> B}) := Fun.copy inv f^-1. HB.instance Definition _ {f : {splitsurj A >-> B}} := Inv_Can.Build _ _ _ f^-1 'invK_f. @@ -581,7 +581,7 @@ Lemma some_canV_subproof : OInv_CanV _ _ A (some @` A) (@Some T). Proof. by split=> [x|x /set_mem] [a Aa <-]//=; exists a. Qed. HB.instance Definition _ := some_canV_subproof. -Lemma some_fun_subproof : IsFun _ _ A (some @` A) (@Some T). +Lemma some_fun_subproof : isFun _ _ A (some @` A) (@Some T). Proof. by split=> x; exists x. Qed. HB.instance Definition _ := some_fun_subproof. @@ -611,7 +611,7 @@ by split=> [b|b /set_mem] Bb/=; rewrite inv_oapp; case: oinvP => // x; exists x. Qed. HB.instance Definition _ f := oapp_surj_subproof f. -Lemma oapp_fun_subproof (f : {fun A >-> B}) : IsFun _ _ (some @` A) B (oapp f). +Lemma oapp_fun_subproof (f : {fun A >-> B}) : isFun _ _ (some @` A) B (oapp f). Proof. by split=> x [a Aa <-] /=; apply: funS. Qed. HB.instance Definition _ f := oapp_fun_subproof f. HB.instance Definition _ (f : {oinvfun A >-> B}) := Fun.on (oapp f). @@ -649,7 +649,7 @@ Section Composition. Context {aT rT sT} {A : set aT} {B : set rT} {C : set sT}. Local Lemma comp_fun_subproof (f : {fun A >-> B}) (g : {fun B >-> C}) : - IsFun _ _ A C (g \o f). + isFun _ _ A C (g \o f). Proof. by split => x /'funS_f; apply: funS. Qed. HB.instance Definition _ f g := comp_fun_subproof f g. @@ -712,7 +712,7 @@ Definition totalfun_ (A : set aT) (f : aT -> rT) := f. Context {A : set aT}. Local Notation totalfun := (totalfun_ A). HB.instance Definition _ (f : aT -> rT) := - IsFun.Build _ _ A setT (totalfun f) (fun _ _ => I). + isFun.Build _ _ A setT (totalfun f) (fun _ _ => I). HB.instance Definition _ (f : {inj A >-> rT}) := Inject.on (totalfun f). HB.instance Definition _ (f : {splitinj A >-> rT}) := SplitInj.on (totalfun f). HB.instance Definition _ (f : {surj A >-> [set: rT]}) := @@ -786,7 +786,7 @@ HB.factory Record OInv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of oinvK : {in B, ocancel 'oinv_f f}; }. HB.builders Context {aT rT} A B (f : aT -> rT) of OInv_Can2 _ _ A B f. - HB.instance Definition _ := IsFun.Build aT rT _ _ f funS. + HB.instance Definition _ := isFun.Build aT rT _ _ f funS. HB.instance Definition _ := OInv_Can.Build aT rT _ f funoK. HB.instance Definition _ := OInv_CanV.Build aT rT _ _ f oinvS oinvK. HB.end. @@ -818,7 +818,7 @@ HB.factory Record Inv_Can2 {aT rT} {A : set aT} {B : set rT} (f : aT -> rT) of invK : {in B, cancel f^-1 f}; }. HB.builders Context {aT rT} A B (f : aT -> rT) of Inv_Can2 _ _ A B f. - HB.instance Definition _ := IsFun.Build aT rT A B f funS. + HB.instance Definition _ := isFun.Build aT rT A B f funS. HB.instance Definition _ := Inv_Can.Build aT rT A f funK. HB.instance Definition _ := @Inv_CanV.Build aT rT A B f invS invK. HB.end. @@ -912,7 +912,7 @@ Lemma set_fun_image : set_fun A (f @` A) f. Proof. exact/image_subP. Qed. HB.instance Definition _ := - @IsFun.Build _ _ _ _ (funin A f) set_fun_image. + @isFun.Build _ _ _ _ (funin A f) set_fun_image. HB.instance Definition _ : OCanV _ _ A (f @` A) (funin A f) := ((fun _ => id) : set_surj A (f @` A) f). @@ -1024,7 +1024,7 @@ Section Pfun. Context {aT rT} {A : set aT} {B : set rT} {f : aT -> rT} (ffun : {homo f : x / A x >-> B x}). Let g : _ -> _ := f. -#[local] HB.instance Definition _ := IsFun.Build _ _ _ _ g ffun. +#[local] HB.instance Definition _ := isFun.Build _ _ _ _ g ffun. Lemma Pfun : {i : {fun A >-> B} | f = i}. Proof. by exists [fun of g]. Qed. End Pfun. @@ -1033,7 +1033,7 @@ Context {aT rT} {A : set aT} {B : set rT} {f : {inj A >-> rT}} (ffun : {homo f : x / A x >-> B x}). Let g : _ -> _ := f. #[local] HB.instance Definition _ := Inject.on g. -#[local] HB.instance Definition _ := IsFun.Build _ _ A B g ffun. +#[local] HB.instance Definition _ := isFun.Build _ _ A B g ffun. Lemma injPfun : {i : {injfun A >-> B} | f = i :> (_ -> _)}. Proof. by exists [injfun of g]. Qed. End injPfun. @@ -1063,7 +1063,7 @@ Context {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}} (ffun : {homo f : x / A x >-> B x}). Let g : _ -> _ := f. #[local] HB.instance Definition _ := Surject.on g. -#[local] HB.instance Definition _ := IsFun.Build _ _ A B g ffun. +#[local] HB.instance Definition _ := isFun.Build _ _ A B g ffun. Lemma surjPfun : {s : {surjfun A >-> B} | f = s :> (_ -> _)}. Proof. by exists [surjfun of g]. Qed. End surjPfun. @@ -1123,8 +1123,8 @@ Section iter_inv. Context {aT} {A : set aT}. -Local Lemma iter_fun_subproof n (f : {fun A >-> A}) : IsFun _ _ A A (iter n f). -Proof. +Local Lemma iter_fun_subproof n (f : {fun A >-> A}) : isFun _ _ A A (iter n f). +Proof. split => x; elim: n => // n /[apply] ?; apply/(fun_image_sub f). by exists (iter n f x). Qed. @@ -1133,7 +1133,7 @@ HB.instance Definition _ n f := iter_fun_subproof n f. Section OInv. Context {f : {oinv aT >-> aT}}. -HB.instance Definition _ n := OInv.Build _ _ (iter n f) +HB.instance Definition _ n := OInv.Build _ _ (iter n f) (iter n (obind 'oinv_f) \o some). Lemma oinv_iter n : 'oinv_(iter n f) = iter n (obind 'oinv_f) \o some. Proof. by []. Qed. @@ -1152,9 +1152,9 @@ Lemma inv_iter n : (iter n f)^-1 = iter n f^-1. Proof. by []. Qed. End OInv. Lemma iter_can_subproof n (f : {injfun A >-> A}) : OInv_Can aT aT A (iter n f). -Proof. +Proof. split=> x Ax; rewrite oinv_iter /=; elim: n=> // n IH. -rewrite iterfSr /= funoK //; exact: mem_fun. +by rewrite iterfSr /= funoK //; exact: mem_fun. Qed. HB.instance Definition _ f g := iter_can_subproof f g. @@ -1193,7 +1193,7 @@ Section Unbind. Context {aT rT} {A : set aT} {B : set rT} (dflt : aT -> rT). Definition unbind (f : aT -> option rT) x := odflt (dflt x) (f x). -Lemma unbind_fun_subproof (f : {fun A >-> some @` B}) : IsFun _ _ A B (unbind f). +Lemma unbind_fun_subproof (f : {fun A >-> some @` B}) : isFun _ _ A B (unbind f). Proof. by rewrite /unbind; split=> x /'funS_f [y Bu <-]. Qed. HB.instance Definition _ f := unbind_fun_subproof f. @@ -1295,7 +1295,7 @@ Definition to_setT {T} (x : T) : [set: T] := @SigSub _ _ _ x (mem_set I : x \in setT). HB.instance Definition _ T := Can.Build T [set: T] setT to_setT ((fun _ _ => erefl) : {in setT, cancel to_setT val}). -HB.instance Definition _ T := IsFun.Build T _ setT setT to_setT (fun _ _ => I). +HB.instance Definition _ T := isFun.Build T _ setT setT to_setT (fun _ _ => I). HB.instance Definition _ T := SplitInjFun_CanV.Build T _ _ _ to_setT (fun x y => I) inj. Definition setTbij {T} := [splitbij of @to_setT T]. @@ -1368,7 +1368,7 @@ Context {T} {A B : set T}. Definition incl (AB : A `<=` B) := @id T. HB.instance Definition _ (AB : A `<=` B) := Inv.Build _ _ (incl AB) id. -HB.instance Definition _ (AB : A `<=` B) := IsFun.Build _ _ A B (incl AB) AB. +HB.instance Definition _ (AB : A `<=` B) := isFun.Build _ _ A B (incl AB) AB. HB.instance Definition _ (AB : A `<=` B) := Inv_Can.Build _ _ A (incl AB) (fun _ _ => erefl). @@ -1389,7 +1389,7 @@ Section mkfun. Context {aT} {rT} {A : set aT} {B : set rT}. Notation isfun f := {homo f : x / A x >-> B x}. Definition mkfun f (fAB : isfun f) := f. -HB.instance Definition _ f fAB := @IsFun.Build _ _ A B (@mkfun f fAB) fAB. +HB.instance Definition _ f fAB := @isFun.Build _ _ A B (@mkfun f fAB) fAB. Definition mkfun_fun f fAB := [fun of @mkfun f fAB]. HB.instance Definition _ (f : {inj A >-> rT}) fAB := Inject.on (@mkfun f fAB). HB.instance Definition _ (f : {splitinj A >-> rT}) fAB := @@ -1431,7 +1431,7 @@ Definition ssquash {T} := [splitsurj of @squash T]. HB.instance Definition _ (T : countType) := Inj.Build _ _ setT (@choice.pickle T) (in2W (pcan_inj choice.pickleK)). HB.instance Definition _ (T : countType) := - IsFun.Build _ _ setT setT (@choice.pickle T) (fun _ _ => I). + isFun.Build _ _ setT setT (@choice.pickle T) (fun _ _ => I). (***********) (* set0fun *) @@ -1443,7 +1443,7 @@ Proof. by case=> x x0; have := set_mem x0. Qed. HB.instance Definition _ P T := Inj.Build (@set0 T) P setT set0fun (in2W set0fun_inj). HB.instance Definition _ P T := - IsFun.Build _ _ setT setT (@set0fun P T) (fun _ _ => I). + isFun.Build _ _ setT setT (@set0fun P T) (fun _ _ => I). (************) (* cast_ord *) @@ -1527,7 +1527,7 @@ Context {XY : [disjoint X & Y]} {AB : [disjoint A & B]}. Local Notation gl := (glue XY AB). Lemma glue_fun_subproof (f : {fun X >-> A}) (g : {fun Y >-> B}) : - IsFun T T' (X `|` Y) (A `|` B) (gl f g). + isFun T T' (X `|` Y) (A `|` B) (gl f g). Proof. by split=> x []xP; [left; rewrite glue1|right; rewrite glue2]; rewrite ?inE//; apply: funS. @@ -1643,7 +1643,7 @@ Lemma empty_can_subproof : OInv_Can T T' X any. Proof. by split=> x; rewrite empty_eq0 inE. Qed. HB.instance Definition _ := empty_can_subproof. -Lemma empty_fun_subproof Y : IsFun T T' X Y any. +Lemma empty_fun_subproof Y : isFun T T' X Y any. Proof. by split=> x; rewrite empty_eq0. Qed. HB.instance Definition _ Y := empty_fun_subproof Y. @@ -1821,7 +1821,7 @@ Lemma set_bij_sub : f @` A `<=` B. Proof. exact/image_subP/set_bij_homo. Qed. Lemma set_bij_surj : set_surj A B f. Proof. by case: fbij. Qed. HB.instance Definition _ : OCanV _ _ _ _ g := set_bij_surj. -HB.instance Definition _ := IsFun.Build _ _ A B g set_bij_homo. +HB.instance Definition _ := isFun.Build _ _ A B g set_bij_homo. HB.instance Definition _ := SurjFun_Inj.Build _ _ A B g set_bij_inj. End set_bij_lemmas. @@ -1965,7 +1965,7 @@ Local Notation restrict := (patch (fun=> v) A). Definition sigL (f : U -> V) : A -> V := f \o set_val. -Lemma sigL_isfun (f : {fun A >-> B}) : IsFun _ _ [set: A] B (sigL f). +Lemma sigL_isfun (f : {fun A >-> B}) : isFun _ _ [set: A] B (sigL f). Proof. by split=> x _; apply: funS. Qed. HB.instance Definition _ (f : {fun A >-> B}) := sigL_isfun f. @@ -1973,7 +1973,7 @@ Definition sigLfun (f : {fun A >-> B}) := [fun of sigL f]. Definition valL_ (f : A -> V) : U -> V := ((@oapp _ _)^~ v) f \o 'oinv_set_val. Lemma valL_isfun (f : {fun [set: A] >-> B}) : - IsFun _ _ A B (valL_ (f : _ -> _)). + isFun _ _ A B (valL_ (f : _ -> _)). Proof. by split=> x Ax; apply: funS. Qed. HB.instance Definition _ (f : {fun [set: A] >-> B}) := valL_isfun f. Definition valLfun_ (f : {fun [set: A] >-> B}) := [fun of valL_ f]. @@ -2569,7 +2569,7 @@ Section injpPfun. Context {B : set U} {f : {inj A >-> U}} (ffun : {homo f : x / A x >-> B x}). Let g : _ -> _ := f. #[local] HB.instance Definition _ := SplitInj.copy g ('split_dflt [fun g in A]). -#[local] HB.instance Definition _ := IsFun.Build _ _ _ _ g ffun. +#[local] HB.instance Definition _ := isFun.Build _ _ _ _ g ffun. Lemma injpPfun_ : {i : {splitinjfun A >-> B} | f = i :> (_ -> _)}. Proof. by exists [splitinjfun of g]. Qed. End injpPfun. diff --git a/theories/realfun.v b/theories/realfun.v index 387d4c684..4d439748c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -196,7 +196,7 @@ Qed. Section negation_itv. Local Definition itvN_oppr a b := @GRing.opp R. Local Lemma itv_oppr_is_fun a b : - IsFun _ _ `[- b, - a]%classic `[a, b]%classic (itvN_oppr a b). + isFun _ _ `[- b, - a]%classic `[a, b]%classic (itvN_oppr a b). Proof. by split=> x /=; rewrite oppr_itvcc. Qed. HB.instance Definition _ a b := itv_oppr_is_fun a b. End negation_itv. From f036e8fb5c9b82681356866ac10150ae138b5428 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 14 Mar 2023 11:38:36 +0900 Subject: [PATCH 3/4] fixes #864 --- theories/topology.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/topology.v b/theories/topology.v index 70cd51c68..0f5425e7e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -254,7 +254,7 @@ Require Import reals signed. (* {uniform, F --> f} := {uniform setT, F --> f} *) (* {ptws U -> V} == The space U -> V, equipped with the topology of *) (* pointwise convergence from U to V, where V is a *) -(* topologicalType. *) +(* topologicalType; notation for @fct_Pointwise U V. *) (* {ptws, F --> f} == F converges to f in {ptws U -> V}. *) (* {family fam, U -> V} == The space U -> V, equipped with the supremum *) (* topology of {uniform A -> f} for each A in 'fam' *) From 1e7533dcca403b9b952a9776dfdfc3766dbf1525 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 14 Mar 2023 12:07:23 +0900 Subject: [PATCH 4/4] fix changelog --- CHANGELOG_UNRELEASED.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index bfb5bf0d8..0f3914b6e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -37,6 +37,8 @@ + `PseudoMetric.ax2` -> `PseudoMetric.ball_sym` + `PseudoMetric.ax3` -> `PseudoMetric.ball_triangle` + `PseudoMetric.ax4` -> `PseudoMetric.entourageE` +- in `functions.v`: + + `IsFun` -> `isFun` ### Generalized