From 2b42967813db430ecb1581f6cd9d5c5323cf9bf0 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 19 Jun 2020 15:26:19 +0900 Subject: [PATCH] Generalize prod_pseudoMetricNormedZmodType --- theories/normedtype.v | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 56b48388d8..016e1fabd8 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2656,11 +2656,8 @@ End matrix_NormedModule. (** ** Pairs *) -Section prod_NormedModule. -Context {K : numDomainType} {U V : normedModType K}. - -Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. -Proof. by rewrite prod_normE /= !normmZ maxr_pmulr. Qed. +Section prod_PseudoMetricNormedZmodule. +Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. Lemma ball_prod_normE : ball = ball_ (fun x => `| x : U * V |). Proof. @@ -2672,10 +2669,18 @@ Qed. Lemma prod_norm_ball : @ball _ [pseudoMetricType K of U * V] = ball_ (fun x => `|x|). Proof. by rewrite /= - ball_prod_normE. Qed. -Definition prod_PseudoMetricNormedZmodMixin := +Definition prod_pseudoMetricNormedZmodMixin := PseudoMetricNormedZmodule.Mixin prod_norm_ball. -Canonical prod_topologicalZmodType := - PseudoMetricNormedZmodType K (U * V) prod_PseudoMetricNormedZmodMixin. +Canonical prod_pseudoMetricNormedZmodType := + PseudoMetricNormedZmodType K (U * V) prod_pseudoMetricNormedZmodMixin. + +End prod_PseudoMetricNormedZmodule. + +Section prod_NormedModule. +Context {K : numDomainType} {U V : normedModType K}. + +Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |. +Proof. by rewrite prod_normE /= !normmZ maxr_pmulr. Qed. Definition prod_NormedModMixin := NormedModMixin prod_norm_scale. Canonical prod_normedModType :=