convex -> convex_set

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -84,7 +84,7 @@
 - in `separation_axioms.v`:
   + lemmas `limit_point_closed`
 - in `convex.v`:
-  + lemma `convexW`
+  + lemma `convex_setW`
 
 ### Changed
 
@@ -244,7 +244,7 @@
   + lemma `ball_open_nbhs`
 
 - moved from `tvs.v` to `convex.v`
-  + definition `convex`
+  + definition `convex`, renamed to `convex_set`
 
 ### Renamed
 

theories/convex.v

@@ -220,13 +220,15 @@ Proof. by move=> ab; rewrite in_itv/= -lerN2 convN convC !conv_le ?lerN2. Qed.
 
 End conv_numDomainType.
 
-Definition convex (R : numDomainType) (M : lmodType R)
+Definition convex_set (R : numDomainType) (M : lmodType R)
     (A : set (convex_lmodType M)) :=
   forall x y lambda, x \in A -> y \in A -> x <| lambda |> y \in A.
 
-Lemma convexW (R : numDomainType) (M : lmodType R) (A : set (convex_lmodType M)) :
-  convex A <->
-  {in A &, forall x y (k : {i01 R}), 0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.
+Lemma convex_setW (R : numDomainType) (M : lmodType R)
+    (A : set (convex_lmodType M)) :
+  convex_set A <->
+  {in A &, forall x y (k : {i01 R}),
+    0 < k%:num -> k%:num < 1 -> x <| k |> y \in A}.
 Proof.
 split => [cA x y xA yA k k0 k1|cA x y l xA yA].
   by have /(_ k) := cA _ _ _ xA yA.
@@ -237,7 +239,8 @@ apply: cA => //.
 - by rewrite lt_neqAle l1 le1.
 Qed.
 
-Definition convex_function (R : numFieldType) (E : lmodType R) (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
+Definition convex_function (R : numFieldType) (E : lmodType R)
+    (E' := convex_lmodType E) (D : set E') (f : E' -> R^o) :=
   forall (t : {i01 R}),
     {in D &, forall (x y : E'), (f (x <| t |> y) <= f x <| t |> f y)%R}.
 (* TODO: generalize to convTypes once we have ordered convTypes (mathcomp 2) *)

theories/normedtype_theory/normed_module.v

@@ -113,9 +113,9 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let ball_convex (x : convex_lmodType V) (r : K) : convex (ball x r).
+Let ball_convex_set (x : convex_lmodType V) (r : K) : convex_set (ball x r).
 Proof.
-apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
 rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
                             (x - y : convex_lmodType _)); last first.
@@ -127,11 +127,12 @@ by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
 (** NB: we have almost the same proof in `tvs.v` *)
-Let locally_convex :
-  exists2 B : set (set (convex_lmodType V)), (forall b, b \in B -> convex b) & basis B.
+Let locally_convex_set :
+  exists2 B : set_system (convex_lmodType V),
+    (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 exists [set B | exists (x : convex_lmodType V) r, B = ball x r].
-  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex.
+  by move=> b; rewrite inE => [[x]] [r] ->; exact: ball_convex_set.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
@@ -141,7 +142,7 @@ HB.instance Definition _ :=
   PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.
-HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex.
+HB.instance Definition _ := Uniform_isTvs.Build K V locally_convex_set.
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Tvs_isNormedModule.Build K V normrZ.
 

theories/normedtype_theory/tvs.v

@@ -310,8 +310,8 @@ HB.end.
 
 HB.mixin Record Uniform_isTvs (R : numDomainType) E
     & Uniform E & GRing.Lmodule R E := {
-  locally_convex : exists2 B : set (set E),
-    (forall b, b \in B -> convex b) & basis B
+  locally_convex : exists2 B : set_system E,
+    (forall b, b \in B -> convex_set b) & basis B
 }.
 
 #[short(type="tvsType")]
@@ -358,8 +358,8 @@ HB.factory Record PreTopologicalLmod_isTvs (R : numDomainType) E
     & Topological E & GRing.Lmodule R E := {
   add_continuous : continuous (fun x : E * E => x.1 + x.2) ;
   scale_continuous : continuous (fun z : R^o * E => z.1 *: z.2) ;
-  locally_convex : exists2 B : set (set E),
-    (forall b, b \in B -> convex b) & basis B
+  locally_convex : exists2 B : set_system E,
+    (forall b, b \in B -> convex_set b) & basis B
   }.
 
 HB.builders Context R E & PreTopologicalLmod_isTvs R E.
@@ -511,9 +511,9 @@ Unshelve. all: by end_near. Qed.
 
 Local Open Scope convex_scope.
 
-Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r).
+Let standard_ball_convex_set (x : R^o) (r : R) : convex_set (ball x r).
 Proof.
-apply/convexW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
+apply/convex_setW => z y; rewrite !inE -!ball_normE /= => zx yx l l0 l1.
 rewrite inE/=.
 rewrite [X in `|X|](_ : _ = (x - z : convex_lmodType _) <| l |>
                             (x - y : convex_lmodType _)); last first.
@@ -524,11 +524,11 @@ rewrite -[ltRHS]mul1r -(add_onemK l%:num) [ltRHS]mulrDl.
 by rewrite ltrD// ltr_pM2l// onem_gt0.
 Qed.
 
-Let standard_locally_convex :
-  exists2 B : set (set R^o), (forall b, b \in B -> convex b) & basis B.
+Let standard_locally_convex_set :
+  exists2 B : set_system R^o, (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 exists [set B | exists x r, B = ball x r].
-  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex.
+  by move=> B/= /[!inE]/= [[x]] [r] ->; exact: standard_ball_convex_set.
 split; first by move=> B [x] [r] ->; exact: ball_open.
 move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //=; split; [exists x, r|exact: ballxx].
@@ -538,14 +538,16 @@ HB.instance Definition _ :=
   PreTopologicalNmodule_isTopologicalNmodule.Build R^o standard_add_continuous.
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build R R^o standard_scale_continuous.
-HB.instance Definition _ := Uniform_isTvs.Build R R^o standard_locally_convex.
+HB.instance Definition _ :=
+  Uniform_isTvs.Build R R^o standard_locally_convex_set.
 
 End standard_topology.
 
 Section prod_Tvs.
 Context (K : numFieldType) (E F : tvsType K).
 
-Local Lemma prod_add_continuous : continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
+Local Lemma prod_add_continuous :
+  continuous (fun x : (E * F) * (E * F) => x.1 + x.2).
 Proof.
 move => [/= xy1 xy2] /= U /= [] [A B] /= [nA nB] nU.
 have [/= A0 [A01 A02] nA1] := @add_continuous E (xy1.1, xy2.1) _ nA.
@@ -556,7 +558,8 @@ move => [[x1 y1][x2 y2]] /= [] [] a1 b1 [] a2 b2.
 by apply: nU; split; [exact: (nA1 (x1, x2))|exact: (nB1 (y1, y2))].
 Qed.
 
-Local Lemma prod_scale_continuous : continuous (fun z : K^o * (E * F) => z.1 *: z.2).
+Local Lemma prod_scale_continuous :
+  continuous (fun z : K^o * (E * F) => z.1 *: z.2).
 Proof.
 move => [/= r [x y]] /= U /= []/= [A B] /= [nA nB] nU.
 have [/= A0 [A01 A02] nA1] := @scale_continuous K E (r, x) _ nA.
@@ -568,7 +571,7 @@ by move=> [l [e f]] /= [] [Al Bl] [] Ae Be; apply: nU; split;
 Qed.
 
 Local Lemma prod_locally_convex :
-  exists2 B : set (set (E * F)), (forall b, b \in B -> convex b) & basis B.
+  exists2 B : set_system (E * F), (forall b, b \in B -> convex_set b) & basis B.
 Proof.
 have [Be Bcb Beb] := @locally_convex K E.
 have [Bf Bcf Bfb] := @locally_convex K F.