move structures about functions from landau.v to topology.v

math-comp · May 16, 2019 · 094029b · 094029b
1 parent 8768257
commit 094029b
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 48 deletions.
diff --git a/landau.v b/landau.v
@@ -282,54 +282,6 @@ Local Open Scope ring_scope.
 Local Open Scope real_scope.
 Local Open Scope classical_set_scope.
 
-Section function_space.
-
-Definition cst {T T' : Type} (x : T') : T -> T' := fun=> x.
-
-Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=
-  @ZmodMixin (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g) _ _ _ _.
-Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite addrA. Qed.
-Next Obligation. by move=> f g; rewrite funeqE=> x /=; rewrite addrC. Qed.
-Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite add0r. Qed.
-Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite addNr. Qed.
-Canonical fct_zmodType T (M : zmodType) := ZmodType (T -> M) (fct_zmodMixin T M).
-
-Program Definition fct_ringMixin (T : pointedType) (M : ringType) :=
-  @RingMixin [zmodType of T -> M] (cst 1) (fun f g x => f x * g x)
-             _ _ _ _ _ _.
-Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed.
-Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mul1r. Qed.
-Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mulr1. Qed.
-Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDl. Qed.
-Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDr. Qed.
-Next Obligation.
-by apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0.
-Qed.
-Canonical fct_ringType (T : pointedType) (M : ringType) :=
-  RingType (T -> M) (fct_ringMixin T M).
-
-Program Canonical fct_comRingType (T : pointedType) (M : comRingType) :=
-  ComRingType (T -> M) _.
-Next Obligation. by move=> f g; rewrite funeqE => x; rewrite mulrC. Qed.
-
-Program Definition fct_lmodMixin (U : Type) (R : ringType) (V : lmodType R)
-  := @LmodMixin R [zmodType of U -> V] (fun k f => k \*: f) _ _ _ _.
-Next Obligation. rewrite funeqE => x; exact: scalerA. Qed.
-Next Obligation. by move=> f; rewrite funeqE => x /=; rewrite scale1r. Qed.
-Next Obligation. by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. Qed.
-Next Obligation. by move=> f g; rewrite funeqE => x /=; rewrite scalerDl. Qed.
-Canonical fct_lmodType U (R : ringType) (V : lmodType R) :=
-  LmodType _ (U -> V) (fct_lmodMixin U V).
-
-Lemma fct_sumE (T : Type) (M : zmodType) n (f : 'I_n -> T -> M) (x : T) :
-  (\sum_(i < n) f i) x = \sum_(i < n) f i x.
-Proof.
-elim: n f => [|n H] f;
-  by rewrite !(big_ord0,big_ord_recr) //= -[LHS]/(_ x + _ x) H.
-Qed.
-
-End function_space.
-
 Section Linear1.
 Context (R : ringType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
 Canonical linear_eqType := EqType {linear U -> V | s} gen_eqMixin.

diff --git a/topology.v b/topology.v
@@ -278,6 +278,54 @@ Unset Printing Implicit Defensive.
 Import GRing.Theory Num.Def Num.Theory.
 Local Open Scope classical_set_scope.
 
+Section function_space.
+
+Definition cst {T T' : Type} (x : T') : T -> T' := fun=> x.
+
+Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=
+  @ZmodMixin (T -> M) \0 (fun f x => - f x) (fun f g => f \+ g) _ _ _ _.
+Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite addrA. Qed.
+Next Obligation. by move=> f g; rewrite funeqE=> x /=; rewrite addrC. Qed.
+Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite add0r. Qed.
+Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite addNr. Qed.
+Canonical fct_zmodType T (M : zmodType) := ZmodType (T -> M) (fct_zmodMixin T M).
+
+Program Definition fct_ringMixin (T : pointedType) (M : ringType) :=
+  @RingMixin [zmodType of T -> M] (cst 1) (fun f g x => f x * g x)
+             _ _ _ _ _ _.
+Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed.
+Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mul1r. Qed.
+Next Obligation. by move=> f; rewrite funeqE=> x /=; rewrite mulr1. Qed.
+Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDl. Qed.
+Next Obligation. by move=> f g h; rewrite funeqE=> x /=; rewrite mulrDr. Qed.
+Next Obligation.
+by apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0.
+Qed.
+Canonical fct_ringType (T : pointedType) (M : ringType) :=
+  RingType (T -> M) (fct_ringMixin T M).
+
+Program Canonical fct_comRingType (T : pointedType) (M : comRingType) :=
+  ComRingType (T -> M) _.
+Next Obligation. by move=> f g; rewrite funeqE => x; rewrite mulrC. Qed.
+
+Program Definition fct_lmodMixin (U : Type) (R : ringType) (V : lmodType R)
+  := @LmodMixin R [zmodType of U -> V] (fun k f => k \*: f) _ _ _ _.
+Next Obligation. rewrite funeqE => x; exact: scalerA. Qed.
+Next Obligation. by move=> f; rewrite funeqE => x /=; rewrite scale1r. Qed.
+Next Obligation. by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr. Qed.
+Next Obligation. by move=> f g; rewrite funeqE => x /=; rewrite scalerDl. Qed.
+Canonical fct_lmodType U (R : ringType) (V : lmodType R) :=
+  LmodType _ (U -> V) (fct_lmodMixin U V).
+
+Lemma fct_sumE (T : Type) (M : zmodType) n (f : 'I_n -> T -> M) (x : T) :
+  (\sum_(i < n) f i) x = \sum_(i < n) f i x.
+Proof.
+elim: n f => [|n H] f;
+  by rewrite !(big_ord0,big_ord_recr) //= -[LHS]/(_ x + _ x) H.
+Qed.
+
+End function_space.
+
 Module Filtered.
 
 (* Index a family of filters on a type, one for each element of the type *)