From c9cd6ac4b93a1701a74dec50e1873a05e260a386 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 26 Dec 2020 06:46:42 +0900 Subject: [PATCH] Fix non-forgetful inheritance --- theories/derive.v | 1 + theories/ereal.v | 9 +- theories/normedtype.v | 1050 ++++++++++++++++++++++++++--------------- theories/sequences.v | 10 +- theories/topology.v | 544 +++++++++++++-------- 5 files changed, 1020 insertions(+), 594 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 4f78cb33d2..a7aecce0d7 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -25,6 +25,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. +Import nonforgetful_inheritance.Exports. Local Open Scope ring_scope. Local Open Scope classical_set_scope. diff --git a/theories/ereal.v b/theories/ereal.v index 0389757f79..c09248ed54 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -58,6 +58,7 @@ Unset Printing Implicit Defensive. Declare Scope ereal_scope. Import Order.TTheory GRing.Theory Num.Theory. +Import nonforgetful_inheritance.Exports. Local Open Scope ring_scope. @@ -220,10 +221,10 @@ Notation "x < y <= z" := ((x < y) && (y <= z)) : ereal_scope. Notation "x <= y < z" := ((x <= y) && (y < z)) : ereal_scope. Notation "x < y < z" := ((x < y) && (y < z)) : ereal_scope. -Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E) = (x <= y)%O. +Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E) = (x <= y)%R. Proof. by []. Qed. -Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%O. +Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%R. Proof. by []. Qed. Lemma lte_pinfty (R : realDomainType) (x : R) : x%:E < +oo. @@ -668,10 +669,10 @@ Lemma le0R (x : {ereal R}) : 0%:E <= x -> (0 <= real_of_er(*TODO: coercion broken*) x)%R. Proof. by case: x. Qed. -Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%O -> r0%:E <= r1%:E. +Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%R -> r0%:E <= r1%:E. Proof. by []. Qed. -Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%O -> r0%:E < r1%:E. +Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R -> r0%:E < r1%:E. Proof. by []. Qed. End ERealOrderTheory. diff --git a/theories/normedtype.v b/theories/normedtype.v index a3ced34aa4..4498d4495f 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -84,6 +84,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import nonforgetful_inheritance.Exports. Local Open Scope ring_scope. Local Open Scope classical_set_scope. @@ -127,323 +128,6 @@ by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE. Qed. End pseudoMetric_of_normedDomain. -Section vecspace_of_numfield. (*NEW*) - (*TODO: put all results on ^o in a separate module (C. Cohen suggestion) *) - (* !! Redundant with ^o *) - (* While there may not be a canonical algebra on each ring, we assume here *) - (* there is a canonical vecspace on each field. We make use of the *) - (* canonical algebraic structures defined on regular algebras in mathcomp *) - -Canonical numField_lmodType (K : numFieldType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical numField_lalgType (K : numFieldType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical numField_algType (K : numFieldType) := - [algType K of K for [algType K of K^o]]. -Canonical numField_comAlgType (K : numFieldType) := [comAlgType K of K]. -Canonical numField_unitAlgType (K : numFieldType) := [unitAlgType K of K]. -Canonical numField_comUnitAlgType (K : numFieldType) := [comUnitAlgType K of K]. -Canonical numField_vectType (K : numFieldType) := - [vectType K of K for [vectType K of K^o]]. -Canonical numField_falgType (K : numFieldType) := [FalgType K of K]. -Canonical numField_fieldExtType (K : numFieldType) := - [fieldExtType K of K for regular_fieldExtType K]. - -Canonical numClosedField_lmodType (K : numClosedFieldType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical numClosedField_lalgType (K : numClosedFieldType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical numClosedField_algType (K : numClosedFieldType) := - [algType K of K for [algType K of K^o]]. -Canonical numClosedField_comAlgType (K : numClosedFieldType) := - [comAlgType K of K]. -Canonical numClosedField_unitAlgType (K : numClosedFieldType) := - [unitAlgType K of K]. -Canonical numClosedField_comUnitAlgType (K : numClosedFieldType) := - [comUnitAlgType K of K]. -Canonical numClosedField_vectType (K : numClosedFieldType) := - [vectType K of K for [vectType K of K^o]]. -Canonical numClosedField_falgType (K : numClosedFieldType) := [FalgType K of K]. -Canonical numClosedField_fieldExtType (K : numClosedFieldType) := - [fieldExtType K of K for regular_fieldExtType K]. - -Canonical realField_lmodType (K : realFieldType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical realField_lalgType (K : realFieldType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical realField_algType (K : realFieldType) := - [algType K of K for [algType K of K^o]]. -Canonical realField_comAlgType (K : realFieldType) := [comAlgType K of K]. -Canonical realField_unitAlgType (K : realFieldType) := [unitAlgType K of K]. -Canonical realField_comUnitAlgType (K : realFieldType) := - [comUnitAlgType K of K]. -Canonical realField_vectType (K : realFieldType) := - [vectType K of K for [vectType K of K^o]]. -Canonical realField_falgType (K : realFieldType) := [FalgType K of K]. -Canonical realField_fieldExtType (K : realFieldType) := - [fieldExtType K of K for regular_fieldExtType K]. - -Canonical archiField_lmodType (K : archiFieldType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical archiField_lalgType (K : archiFieldType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical archiField_algType (K : archiFieldType) := - [algType K of K for [algType K of K^o]]. -Canonical archiField_comAlgType (K : archiFieldType) := [comAlgType K of K]. -Canonical archiField_unitAlgType (K : archiFieldType) := [unitAlgType K of K]. -Canonical archiField_comUnitAlgType (K : archiFieldType) := - [comUnitAlgType K of K]. -Canonical archiField_vectType (K : archiFieldType) := - [vectType K of K for [vectType K of K^o]]. -Canonical archiField_falgType (K : archiFieldType) := [FalgType K of K]. -Canonical archiField_fieldExtType (K : archiFieldType) := - [fieldExtType K of K for regular_fieldExtType K]. - -Canonical rcf_lmodType (K : rcfType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical rcf_lalgType (K : rcfType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical rcf_algType (K : rcfType) := [algType K of K for [algType K of K^o]]. -Canonical rcf_comAlgType (K : rcfType) := [comAlgType K of K]. -Canonical rcf_unitAlgType (K : rcfType) := [unitAlgType K of K] . -Canonical rcf_comUnitAlgType (K : rcfType) := [comUnitAlgType K of K]. -Canonical rcf_vectType (K : rcfType) := - [vectType K of K for [vectType K of K^o]]. -Canonical rcf_falgType (K : rcfType) := [FalgType K of K]. -Canonical rcf_fieldExtType (K : rcfType) := - [fieldExtType K of K for regular_fieldExtType K]. - -Canonical real_lmodType (K : realType) := - [lmodType K of K for [lmodType K of K^o]]. -Canonical real_lalgType (K : realType) := - [lalgType K of K for [lalgType K of K^o]]. -Canonical real_algType (K : realType) := - [algType K of K for [algType K of K^o]]. -Canonical real_comAlgType (K : realType) := [comAlgType K of K]. -Canonical real_unitAlgType (K : realType) := [unitAlgType K of K]. -Canonical real_comUnitAlgType (K : realType) := [comUnitAlgType K of K]. -Canonical real_vectType (K : realType) := - [vectType K of K for [vectType K of K^o]]. -Canonical real_falgType (K : realType) := [FalgType K of K]. -Canonical real_fieldExtType (K : realType) := - [fieldExtType K of K for regular_fieldExtType K]. - - -Coercion numField_lmodType : numFieldType >-> lmodType. -Coercion numField_lalgType : numFieldType >-> lalgType. -Coercion numField_comAlgType : numFieldType >-> comAlgType. (* ambiguous path *) -Coercion numField_unitAlgType : numFieldType >-> unitAlgType. -Coercion numField_comUnitAlgType : numFieldType >-> comUnitAlgType. (* ambiguous path *) -Coercion numField_vectType : numFieldType >-> vectType. -Coercion numField_falgType : numFieldType >-> FalgType. -Coercion numField_fieldExtType : numFieldType >-> fieldExtType. (* ambiguous path *) - - - -(* TODO : other coercions *) - -End vecspace_of_numfield. - - - -(* Section numField_topological. (*New *) *) (** included in topology.v *) -(* (* Variable (R: numFieldType). *) *) -(* (* Canonical numFieldType_pointedType (R: numFieldType) := *) *) -(* (* [pointedType of R for pointed_of_zmodule R]. *) *) -(* (* Canonical numFieldType_filteredType (R: numFieldType) := *) *) -(* (* [filteredType R of R for filtered_of_normedZmod R]. *) *) -(* (* Canonical numFieldType_topologicalType (R: numFieldType) : topologicalType := TopologicalType R *) *) -(* (* (topologyOfEntourageMixin *) *) -(* (* (uniformityOfBallMixin *) *) -(* (* (@nbhs_ball_normE _ [normedZmodType R of R]) *) *) -(* (* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) *) -(* (* Canonical numFieldType_uniformType (R: numFieldType) : uniformType := UniformType R *) *) -(* (* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) *) -(* (* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) *) -(* (* Canonical numFieldType_pseudoMetricType (R: numFieldType) *) *) -(* (* := @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) *) -(* (* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) *) -(* (** the previous is included in topology.v **) *) - -(* Canonical numClosedFieldType_pointedType (R: numClosedFieldType) := *) -(* [pointedType of R for [pointedType of [numFieldType of R]]]. *) -(* Canonical numClosedFieldType_filteredType (R: numClosedFieldType) := *) -(* [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. *) -(* Canonical numClosedFieldType_topologicalType (R: numClosedFieldType) : topologicalType := *) -(* (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) *) -(* (*leads to ambiguous path *) *) -(* TopologicalType R *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical numClosedFieldType_uniformType (R: numClosedFieldType) : uniformType := UniformType R *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical numClosedFieldType_pseudoMetricType (R: numClosedFieldType) := *) -(* (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) *) -(* (* leads to ambiguous path *) *) -(* @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) - -(* Canonical realFieldType_pointedType (R: realFieldType) := *) -(* [pointedType of R for [pointedType of [numFieldType of R]]]. *) -(* Canonical realFieldType_filteredType (R: realFieldType) := *) -(* [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. *) -(* Canonical realFieldType_topologicalType (R: realFieldType) : topologicalType := *) -(* (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) *) -(* (*leads to ambiguous path *) *) -(* TopologicalType R *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical realFieldType_uniformType (R: realFieldType) : uniformType := UniformType R *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical realFieldType_pseudoMetricType (R: realFieldType) := *) -(* (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) *) -(* (* leads to ambiguous path *) *) -(* @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) - -(* Canonical archiFieldType_pointedType (R: archiFieldType) := *) -(* [pointedType of R for [pointedType of [numFieldType of R]]]. *) -(* Canonical archiFieldType_filteredType (R: archiFieldType) := *) -(* [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. *) -(* Canonical archiFieldType_topologicalType (R: archiFieldType) : topologicalType := *) -(* (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) *) -(* (*leads to ambiguous path *) *) -(* TopologicalType R *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical archiFieldType_uniformType (R: archiFieldType) : uniformType := UniformType R *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical archiFieldType_pseudoMetricType (R: archiFieldType):= *) -(* (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) *) -(* (* leads to ambiguous path *) *) -(* @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) - -(* Canonical rcfType_pointedType (R: rcfType) := *) -(* [pointedType of R for [pointedType of [numFieldType of R]]]. *) -(* Canonical rcfType_filteredType (R: rcfType) := *) -(* [filteredType R of R for filtered_of_normedZmod R]. *) -(* Canonical rcfType_topologicalType (R: rcfType) : topologicalType := *) -(* (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) *) -(* (*leads to ambiguous path *) *) -(* TopologicalType R *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical rcfType_uniformType (R: rcfType) : uniformType := UniformType R *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical rcfType_pseudoMetricType (R: rcfType) := *) -(* (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) *) -(* (* leads to ambiguous path *) *) -(* @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) - -(* Canonical realType_pointedType (R: realType) := *) -(* [pointedType of R for [pointedType of [numFieldType of R]]]. *) -(* Canonical realType_filteredType (R: realType) := *) -(* [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. *) -(* Canonical realType_topologicalType (R: realType) : topologicalType := *) -(* (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) *) -(* (*leads to ambiguous path *) *) -(* TopologicalType R *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical realType_uniformType (R: realType) : uniformType := UniformType R *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical realType_pseudoMetricType (R: realType) := *) -(* (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) *) -(* (* leads to ambiguous path *) *) -(* @PseudoMetric.Pack R R (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) - -(* Coercion numFieldType_pointedType : numFieldType >-> pointedType. *) -(* Coercion numFieldType_filteredType : numFieldType >-> filteredType. *) -(* Coercion numFieldType_topologicalType : numFieldType >-> topologicalType. *) -(* Coercion numFieldType_uniformType : numFieldType >-> uniformType. *) -(* Coercion numFieldType_pseudoMetricType : numFieldType >-> pseudoMetricType. *) - -(* Coercion numClosedFieldType_pointedType : numClosedFieldType >-> pointedType. *) -(* Coercion numClosedFieldType_filteredType : numClosedFieldType >-> filteredType. *) -(* Coercion numClosedFieldType_topologicalType : numClosedFieldType >-> topologicalType. *) -(* Coercion numClosedFieldType_uniformType : numClosedFieldType >-> uniformType. *) -(* Coercion numClosedFieldType_pseudoMetricType : numClosedFieldType >-> pseudoMetricType. *) - -(* Coercion realFieldType_pointedType : realFieldType >-> pointedType. *) -(* Coercion realFieldType_filteredType : realFieldType >-> filteredType. *) -(* Coercion realFieldType_topologicalType : realFieldType >-> topologicalType. *) -(* Coercion realFieldType_uniformType : realFieldType >-> uniformType. *) -(* Coercion realFieldType_pseudoMetricType : realFieldType >-> pseudoMetricType. *) - -(* Coercion archiFieldType_pointedType : archiFieldType >-> pointedType. *) -(* Coercion archiFieldType_filteredType : archiFieldType >-> filteredType. *) -(* Coercion archiFieldType_topologicalType : archiFieldType >-> topologicalType. *) -(* Coercion archiFieldType_uniformType : archiFieldType >-> uniformType. *) -(* Coercion archiFieldType_pseudoMetricType : archiFieldType >-> pseudoMetricType. *) - -(* Coercion rcfType_pointedType : rcfType >-> pointedType. *) -(* Coercion rcfType_filteredType : rcfType >-> filteredType. *) -(* Coercion rcfType_topologicalType : rcfType >-> topologicalType. *) -(* Coercion rcfType_uniformType : rcfType >-> uniformType. *) -(* Coercion rcfType_pseudoMetricType : rcfType >-> pseudoMetricType. *) - -(* Coercion realType_pointedType : realType >-> pointedType. *) -(* Coercion realType_filteredType : realType >-> filteredType. *) -(* Coercion realType_topologicalType : realType >-> topologicalType. *) -(* Coercion realType_uniformType : realType >-> uniformType. *) -(* Coercion realType_pseudoMetricType : realType >-> pseudoMetricType. *) - - -(* End numField_topological. *) - - -(* Canonical R_pointedType := [pointedType of *) -(* Rdefinitions.R for pointed_of_zmodule R_ringType]. *) -(* (* NB: similar definition in topology.v *) *) -(* Canonical R_filteredType := [filteredType Rdefinitions.R of *) -(* Rdefinitions.R for filtered_of_normedZmod R_normedZmodType]. *) -(* Canonical R_topologicalType : topologicalType := TopologicalType Rdefinitions.R *) -(* (topologyOfBallMixin (pseudoMetric_of_normedDomain R_normedZmodType)). *) -(* Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType := *) -(* PseudoMetricType Rdefinitions.R (pseudoMetric_of_normedDomain R_normedZmodType). *) - -(* Section numFieldType_regular_canonical. (*Modified *) *) -(* (* TODO: specific module *) *) -(* Variable R : numFieldType. *) -(* (*Canonical topological_of_numFieldType := [numFieldType of R^o].*) *) -(* Canonical numFieldType_regular_pointedType := *) -(* [pointedType of R^o for pointed_of_zmodule R]. *) -(* Canonical numFieldType_regular_filteredType := *) -(* [filteredType R of R^o for filtered_of_normedZmod R]. *) -(* Canonical numFieldType_regular_topologicalType : topologicalType := TopologicalType R^o *) -(* (topologyOfEntourageMixin *) -(* (uniformityOfBallMixin *) -(* (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R]))). *) -(* Canonical numFieldType_regular_uniformType : uniformType := UniformType R^o *) -(* (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) *) -(* (pseudoMetric_of_normedDomain [normedZmodType R of R])). *) -(* Canonical numFieldType_regular_pseudoMetricType := *) -(* @PseudoMetric.Pack R R^o (@PseudoMetric.Class R R *) -(* (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). *) -(* Definition numdFieldType_lalgType : lalgType R := @GRing.regular_lalgType R. *) -(* End numFieldType_regular_canonical. *) - - - Lemma nbhsN (R : numFieldType) (x : R) : nbhs (- x) = [set [set - y | y in A] | A in nbhs x]. Proof. @@ -608,40 +292,6 @@ Proof. by case: V => ? [? ? ? ? ? ? []]. Qed. End pseudoMetricnormedzmodule_lemmas. -Section numFieldType_pseudoMetricNormedZmod. (*modified*) - -Lemma R_ball (R : numFieldType) : - @ball _ [pseudoMetricType R of R] = ball_ (fun x => `| x |). -Proof. by []. Qed. -Definition numFieldType_pseudoMetricNormedZmodMixin (R : numFieldType):= - PseudoMetricNormedZmodule.Mixin (R_ball R). -Canonical numFieldType_pseudoMetricNormedZmodType (R : numFieldType) := - @PseudoMetricNormedZmodType R R (numFieldType_pseudoMetricNormedZmodMixin R). - -(*NEW*) -Canonical numClosedFieldType_PseudoMetricNormedZmodule (R: numClosedFieldType) := - [pseudoMetricNormedZmodType _ of R for - [pseudoMetricNormedZmodType _ of [numFieldType of R]]]. - -Canonical archiFieldType_PseudoMetricNormedZmodule (R: archiFieldType) := - [pseudoMetricNormedZmodType _ of R for - [pseudoMetricNormedZmodType _ of [numFieldType of R]]]. - -Canonical realFieldType_PseudoMetricNormedZmodule (R: realFieldType) := - [pseudoMetricNormedZmodType _ of R for - [pseudoMetricNormedZmodType _ of [numFieldType of R]]]. - -Canonical rcfType_PseudoMetricNormedZmodule (R: rcfType) := - [pseudoMetricNormedZmodType _ of R for - [pseudoMetricNormedZmodType _ of [numFieldType of R]]]. - -Canonical realType_PseudoMetricNormedZmodule (R: realType) := - [pseudoMetricNormedZmodType _ of R for - [pseudoMetricNormedZmodType _ of [numFieldType of R]]]. -(*end NEW*) - -End numFieldType_pseudoMetricNormedZmod. - (** locally *) Section Nbhs'. @@ -652,7 +302,7 @@ Lemma ex_ball_sig (x : T) (P : set T) : {d : {posnum R} | ball x d%:num `<=` ~` P}. Proof. rewrite forallNE notK => exNP. -pose D := [set d : R | d > 0 /\ ball x d `<=` ~` P]. +pose D := [set d : R^o | d > 0 /\ ball x d `<=` ~` P]. have [|d_gt0] := @getPex _ D; last by exists (PosNum d_gt0). by move: exNP => [e eP]; exists e%:num. Qed. @@ -673,7 +323,7 @@ Lemma nbhs_ex (x : T) (P : T -> Prop) : nbhs x P -> {d : {posnum R} | forall y, ball x d%:num y -> P y}. Proof. move=> /nbhs_ballP xP. -pose D := [set d : R | d > 0 /\ forall y, ball x d y -> P y]. +pose D := [set d : R^o | d > 0 /\ forall y, ball x d y -> P y]. have [|d_gt0 dP] := @getPex _ D; last by exists (PosNum d_gt0). by move: xP => [e bP]; exists (e : R). Qed. @@ -1037,54 +687,670 @@ End NormedModule. Export NormedModule.Exports. -Section normedMod_of_numfield. (* NEW !*) - -(* Lemma R_normZ (R : numDomainType) (l : R) (x : R^o) : *) -(* `| l *: x | = `| l | * `| x |. *) -(* Proof. by rewrite normrM. Qed. *) - -(*NB: this is replacing R_normZ above *) -Lemma numDomain_normZ (R : numDomainType) (l : R) (x : R^o) : - `| l *: x | = `| l | * `| x |. -Proof. by rewrite normrM. Qed. - -Lemma numField_normZ (R : numFieldType) (l : R) (x : R) : - `| l *: x | = `| l | * `| x |. -Proof. by rewrite normrM. Qed. +Module regular_topology. -Definition numFieldType_NormedModMixin (R : numFieldType) := - NormedModMixin (@numField_normZ R). - -(* Definition numField_normedModType (R : numFieldType) := *) -(* NormedModType R (numField_lmodType R) (@numField_normedModMixin R). *) -(* (*the only difference is numField_lmodType above *) *) -(* Canonical numField_normedModType. *) -(* Variables (R : numFieldType) (V : normedModType R) (x : R) (w : V). *) -(* Fail Check (x *: w). *) - -(* Canonical numFieldType_normedModType (R : numFieldType) := *) -(* NormedModType R R (numFieldType_NormedModMixin R). *) -(* Canonical realFieldType_normedModType (R : realFieldType) := *) -(* [normedModType R of R for numFieldType_normedModType R]. *) (*fail*) +Section regular_topology. +Local Canonical pseudoMetricNormedZmodType (R : numFieldType) := + @PseudoMetricNormedZmodType + R R^o + (PseudoMetricNormedZmodule.Mixin (erefl : @ball _ R = ball_ Num.norm)). +Local Canonical normedModType (R : numFieldType) := + NormedModType R R^o (@NormedModMixin _ _ ( *:%R : R -> R^o -> _) (@normrM _)). +End regular_topology. +Module Exports. +Canonical pseudoMetricNormedZmodType. +Canonical normedModType. +End Exports. -Canonical regular_numFieldType_normedModType (R : numFieldType) := - NormedModType R R^o (numFieldType_NormedModMixin R). -Canonical numFieldType_normedModType (R : numFieldType) := +End regular_topology. +Export regular_topology.Exports. + +Module nonforgetful_inheritance. + +Section realType. +Variable (R : realType). +Local Canonical real_lmodType := [lmodType R of R for [lmodType R of R^o]]. +Local Canonical real_lalgType := [lalgType R of R for [lalgType R of R^o]]. +Local Canonical real_algType := [algType R of R for [algType R of R^o]]. +Local Canonical real_comAlgType := [comAlgType R of R]. +Local Canonical real_unitAlgType := [unitAlgType R of R]. +Local Canonical real_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical real_vectType := [vectType R of R for [vectType R of R^o]]. +Local Canonical real_FalgType := [FalgType R of R]. +Local Canonical real_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical real_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical real_normedModType := [normedModType R of R for [normedModType R of R^o]]. -Canonical numClosedFieldType_normedModType (R : numClosedFieldType) := +End realType. + +Section rcfType. +Variable (R : rcfType). +Local Canonical rcf_lmodType := [lmodType R of R for [lmodType R of R^o]]. +Local Canonical rcf_lalgType := [lalgType R of R for [lalgType R of R^o]]. +Local Canonical rcf_algType := [algType R of R for [algType R of R^o]]. +Local Canonical rcf_comAlgType := [comAlgType R of R]. +Local Canonical rcf_unitAlgType := [unitAlgType R of R]. +Local Canonical rcf_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical rcf_vectType := [vectType R of R for [vectType R of R^o]]. +Local Canonical rcf_FalgType := [FalgType R of R]. +Local Canonical rcf_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical rcf_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical rcf_normedModType := [normedModType R of R for [normedModType R of R^o]]. -Canonical realFieldType_normedModType (R : realFieldType) := +End rcfType. + +Section archiFieldType. +Variable (R : archiFieldType). +Local Canonical archiField_lmodType := + [lmodType R of R for [lmodType R of R^o]]. +Local Canonical archiField_lalgType := + [lalgType R of R for [lalgType R of R^o]]. +Local Canonical archiField_algType := [algType R of R for [algType R of R^o]]. +Local Canonical archiField_comAlgType := [comAlgType R of R]. +Local Canonical archiField_unitAlgType := [unitAlgType R of R]. +Local Canonical archiField_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical archiField_vectType := + [vectType R of R for [vectType R of R^o]]. +Local Canonical archiField_FalgType := [FalgType R of R]. +Local Canonical archiField_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical archiField_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical archiField_normedModType := [normedModType R of R for [normedModType R of R^o]]. -Canonical archiFieldType_normedModType (R : archiFieldType) := +End archiFieldType. + +Section realFieldType. +Variable (R : realFieldType). +Local Canonical realField_lmodType := [lmodType R of R for [lmodType R of R^o]]. +Local Canonical realField_lalgType := [lalgType R of R for [lalgType R of R^o]]. +Local Canonical realField_algType := [algType R of R for [algType R of R^o]]. +Local Canonical realField_comAlgType := [comAlgType R of R]. +Local Canonical realField_unitAlgType := [unitAlgType R of R]. +Local Canonical realField_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical realField_vectType := [vectType R of R for [vectType R of R^o]]. +Local Canonical realField_FalgType := [FalgType R of R]. +Local Canonical realField_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical realField_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical realField_normedModType := [normedModType R of R for [normedModType R of R^o]]. -Canonical rcfType_normedModType (R : rcfType) := +Definition lmod_latticeType := [latticeType of realField_lmodType]. +Definition lmod_distrLatticeType := [distrLatticeType of realField_lmodType]. +Definition lmod_orderType := [orderType of realField_lmodType]. +Definition lmod_realDomainType := [realDomainType of realField_lmodType]. +Definition lalg_latticeType := [latticeType of realField_lalgType]. +Definition lalg_distrLatticeType := [distrLatticeType of realField_lalgType]. +Definition lalg_orderType := [orderType of realField_lalgType]. +Definition lalg_realDomainType := [realDomainType of realField_lalgType]. +Definition alg_latticeType := [latticeType of realField_algType]. +Definition alg_distrLatticeType := [distrLatticeType of realField_algType]. +Definition alg_orderType := [orderType of realField_algType]. +Definition alg_realDomainType := [realDomainType of realField_algType]. +Definition comAlg_latticeType := [latticeType of realField_comAlgType]. +Definition comAlg_distrLatticeType := + [distrLatticeType of realField_comAlgType]. +Definition comAlg_orderType := [orderType of realField_comAlgType]. +Definition comAlg_realDomainType := [realDomainType of realField_comAlgType]. +Definition unitAlg_latticeType := [latticeType of realField_unitAlgType]. +Definition unitAlg_distrLatticeType := + [distrLatticeType of realField_unitAlgType]. +Definition unitAlg_orderType := [orderType of realField_unitAlgType]. +Definition unitAlg_realDomainType := [realDomainType of realField_unitAlgType]. +Definition comUnitAlg_latticeType := [latticeType of realField_comUnitAlgType]. +Definition comUnitAlg_distrLatticeType := + [distrLatticeType of realField_comUnitAlgType]. +Definition comUnitAlg_orderType := [orderType of realField_comUnitAlgType]. +Definition comUnitAlg_realDomainType := + [realDomainType of realField_comUnitAlgType]. +Definition vect_latticeType := [latticeType of realField_vectType]. +Definition vect_distrLatticeType := [distrLatticeType of realField_vectType]. +Definition vect_orderType := [orderType of realField_vectType]. +Definition vect_realDomainType := [realDomainType of realField_vectType]. +Definition Falg_latticeType := [latticeType of realField_FalgType]. +Definition Falg_distrLatticeType := [distrLatticeType of realField_FalgType]. +Definition Falg_orderType := [orderType of realField_FalgType]. +Definition Falg_realDomainType := [realDomainType of realField_FalgType]. +Definition fieldExt_latticeType := [latticeType of realField_fieldExtType]. +Definition fieldExt_distrLatticeType := + [distrLatticeType of realField_fieldExtType]. +Definition fieldExt_orderType := [orderType of realField_fieldExtType]. +Definition fieldExt_realDomainType := + [realDomainType of realField_fieldExtType]. +Definition pseudoMetricNormedZmod_latticeType := + [latticeType of realField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_distrLatticeType := + [distrLatticeType of realField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_orderType := + [orderType of realField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_realDomainType := + [realDomainType of realField_pseudoMetricNormedZmodType]. +Definition normedMod_latticeType := [latticeType of realField_normedModType]. +Definition normedMod_distrLatticeType := + [distrLatticeType of realField_normedModType]. +Definition normedMod_orderType := [orderType of realField_normedModType]. +Definition normedMod_realDomainType := + [realDomainType of realField_normedModType]. +End realFieldType. + +Section numClosedFieldType. +Variable (R : numClosedFieldType). +Local Canonical numClosedField_lmodType := + [lmodType R of R for [lmodType R of R^o]]. +Local Canonical numClosedField_lalgType := + [lalgType R of R for [lalgType R of R^o]]. +Local Canonical numClosedField_algType := + [algType R of R for [algType R of R^o]]. +Local Canonical numClosedField_comAlgType := [comAlgType R of R]. +Local Canonical numClosedField_unitAlgType := [unitAlgType R of R]. +Local Canonical numClosedField_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical numClosedField_vectType := + [vectType R of R for [vectType R of R^o]]. +Local Canonical numClosedField_FalgType := [FalgType R of R]. +Local Canonical numClosedField_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical numClosedField_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical numClosedField_normedModType := [normedModType R of R for [normedModType R of R^o]]. -Canonical realType_normedModType (R : realType) := +Definition lmod_decFieldType := [decFieldType of numClosedField_lmodType]. +Definition lmod_closedFieldType := [closedFieldType of numClosedField_lmodType]. +Definition lalg_decFieldType := [decFieldType of numClosedField_lalgType]. +Definition lalg_closedFieldType := [closedFieldType of numClosedField_lalgType]. +Definition alg_decFieldType := [decFieldType of numClosedField_algType]. +Definition alg_closedFieldType := [closedFieldType of numClosedField_algType]. +Definition comAlg_decFieldType := [decFieldType of numClosedField_comAlgType]. +Definition comAlg_closedFieldType := + [closedFieldType of numClosedField_comAlgType]. +Definition unitAlg_decFieldType := [decFieldType of numClosedField_unitAlgType]. +Definition unitAlg_closedFieldType := + [closedFieldType of numClosedField_unitAlgType]. +Definition comUnitAlg_decFieldType := + [decFieldType of numClosedField_comUnitAlgType]. +Definition comUnitAlg_closedFieldType := + [closedFieldType of numClosedField_comUnitAlgType]. +Definition vect_decFieldType := [decFieldType of numClosedField_vectType]. +Definition vect_closedFieldType := [closedFieldType of numClosedField_vectType]. +Definition Falg_decFieldType := [decFieldType of numClosedField_FalgType]. +Definition Falg_closedFieldType := [closedFieldType of numClosedField_FalgType]. +Definition fieldExt_decFieldType := + [decFieldType of numClosedField_fieldExtType]. +Definition fieldExt_closedFieldType := + [closedFieldType of numClosedField_fieldExtType]. +Definition pseudoMetricNormedZmod_decFieldType := + [decFieldType of numClosedField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_closedFieldType := + [closedFieldType of numClosedField_pseudoMetricNormedZmodType]. +Definition normedMod_decFieldType := + [decFieldType of numClosedField_normedModType]. +Definition normedMod_closedFieldType := + [closedFieldType of numClosedField_normedModType]. +End numClosedFieldType. + +Section numFieldType. +Variable (R : numFieldType). +Local Canonical numField_lmodType := [lmodType R of R for [lmodType R of R^o]]. +Local Canonical numField_lalgType := [lalgType R of R for [lalgType R of R^o]]. +Local Canonical numField_algType := [algType R of R for [algType R of R^o]]. +Local Canonical numField_comAlgType := [comAlgType R of R]. +Local Canonical numField_unitAlgType := [unitAlgType R of R]. +Local Canonical numField_comUnitAlgType := [comUnitAlgType R of R]. +Local Canonical numField_vectType := [vectType R of R for [vectType R of R^o]]. +Local Canonical numField_FalgType := [FalgType R of R]. +Local Canonical numField_fieldExtType := + [fieldExtType R of R for [fieldExtType R of R^o]]. +Local Canonical numField_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of R for [pseudoMetricNormedZmodType R of R^o]]. +Local Canonical numField_normedModType := [normedModType R of R for [normedModType R of R^o]]. -(*TODO : define without R^o ? Missing joins ? *) -End normedMod_of_numfield. +Definition lmod_porderType := [porderType of numField_lmodType]. +Definition lmod_numDomainType := [numDomainType of numField_lmodType]. +Definition lalg_pointedType := [pointedType of numField_lalgType]. +Definition lalg_filteredType := [filteredType R of numField_lalgType]. +Definition lalg_topologicalType := [topologicalType of numField_lalgType]. +Definition lalg_uniformType := [uniformType of numField_lalgType]. +Definition lalg_pseudoMetricType := [pseudoMetricType R of numField_lalgType]. +Definition lalg_normedZmodType := [normedZmodType R of numField_lalgType]. +Definition lalg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_lalgType]. +Definition lalg_normedModType := [normedModType R of numField_lalgType]. +Definition lalg_porderType := [porderType of numField_lalgType]. +Definition lalg_numDomainType := [numDomainType of numField_lalgType]. +Definition alg_pointedType := [pointedType of numField_algType]. +Definition alg_filteredType := [filteredType R of numField_algType]. +Definition alg_topologicalType := [topologicalType of numField_algType]. +Definition alg_uniformType := [uniformType of numField_algType]. +Definition alg_pseudoMetricType := [pseudoMetricType R of numField_algType]. +Definition alg_normedZmodType := [normedZmodType R of numField_algType]. +Definition alg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_algType]. +Definition alg_normedModType := [normedModType R of numField_algType]. +Definition alg_porderType := [porderType of numField_algType]. +Definition alg_numDomainType := [numDomainType of numField_algType]. +Definition comAlg_pointedType := [pointedType of numField_comAlgType]. +Definition comAlg_filteredType := [filteredType R of numField_comAlgType]. +Definition comAlg_topologicalType := [topologicalType of numField_comAlgType]. +Definition comAlg_uniformType := [uniformType of numField_comAlgType]. +Definition comAlg_pseudoMetricType := + [pseudoMetricType R of numField_comAlgType]. +Definition comAlg_normedZmodType := [normedZmodType R of numField_comAlgType]. +Definition comAlg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_comAlgType]. +Definition comAlg_normedModType := [normedModType R of numField_comAlgType]. +Definition comAlg_porderType := [porderType of numField_comAlgType]. +Definition comAlg_numDomainType := [numDomainType of numField_comAlgType]. +Definition unitAlg_pointedType := [pointedType of numField_unitAlgType]. +Definition unitAlg_filteredType := [filteredType R of numField_unitAlgType]. +Definition unitAlg_topologicalType := [topologicalType of numField_unitAlgType]. +Definition unitAlg_uniformType := [uniformType of numField_unitAlgType]. +Definition unitAlg_pseudoMetricType := + [pseudoMetricType R of numField_unitAlgType]. +Definition unitAlg_normedZmodType := [normedZmodType R of numField_unitAlgType]. +Definition unitAlg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_unitAlgType]. +Definition unitAlg_normedModType := [normedModType R of numField_unitAlgType]. +Definition unitAlg_porderType := [porderType of numField_unitAlgType]. +Definition unitAlg_numDomainType := [numDomainType of numField_unitAlgType]. +Definition comUnitAlg_pointedType := [pointedType of numField_comUnitAlgType]. +Definition comUnitAlg_filteredType := + [filteredType R of numField_comUnitAlgType]. +Definition comUnitAlg_topologicalType := + [topologicalType of numField_comUnitAlgType]. +Definition comUnitAlg_uniformType := [uniformType of numField_comUnitAlgType]. +Definition comUnitAlg_pseudoMetricType := + [pseudoMetricType R of numField_comUnitAlgType]. +Definition comUnitAlg_normedZmodType := + [normedZmodType R of numField_comUnitAlgType]. +Definition comUnitAlg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_comUnitAlgType]. +Definition comUnitAlg_normedModType := + [normedModType R of numField_comUnitAlgType]. +Definition comUnitAlg_porderType := [porderType of numField_comUnitAlgType]. +Definition comUnitAlg_numDomainType := + [numDomainType of numField_comUnitAlgType]. +Definition vect_pointedType := [pointedType of numField_vectType]. +Definition vect_filteredType := [filteredType R of numField_vectType]. +Definition vect_topologicalType := [topologicalType of numField_vectType]. +Definition vect_uniformType := [uniformType of numField_vectType]. +Definition vect_pseudoMetricType := [pseudoMetricType R of numField_vectType]. +Definition vect_normedZmodType := [normedZmodType R of numField_vectType]. +Definition vect_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_vectType]. +Definition vect_normedModType := [normedModType R of numField_vectType]. +Definition vect_porderType := [porderType of numField_vectType]. +Definition vect_numDomainType := [numDomainType of numField_vectType]. +Definition Falg_pointedType := [pointedType of numField_FalgType]. +Definition Falg_filteredType := [filteredType R of numField_FalgType]. +Definition Falg_topologicalType := [topologicalType of numField_FalgType]. +Definition Falg_uniformType := [uniformType of numField_FalgType]. +Definition Falg_pseudoMetricType := [pseudoMetricType R of numField_FalgType]. +Definition Falg_normedZmodType := [normedZmodType R of numField_FalgType]. +Definition Falg_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_FalgType]. +Definition Falg_normedModType := [normedModType R of numField_FalgType]. +Definition Falg_porderType := [porderType of numField_FalgType]. +Definition Falg_numDomainType := [numDomainType of numField_FalgType]. +Definition fieldExt_pointedType := [pointedType of numField_fieldExtType]. +Definition fieldExt_filteredType := [filteredType R of numField_fieldExtType]. +Definition fieldExt_topologicalType := + [topologicalType of numField_fieldExtType]. +Definition fieldExt_uniformType := [uniformType of numField_fieldExtType]. +Definition fieldExt_pseudoMetricType := + [pseudoMetricType R of numField_fieldExtType]. +Definition fieldExt_normedZmodType := + [normedZmodType R of numField_fieldExtType]. +Definition fieldExt_pseudoMetricNormedZmodType := + [pseudoMetricNormedZmodType R of numField_fieldExtType]. +Definition fieldExt_normedModType := [normedModType R of numField_fieldExtType]. +Definition fieldExt_porderType := [porderType of numField_fieldExtType]. +Definition fieldExt_numDomainType := [numDomainType of numField_fieldExtType]. +Definition pseudoMetricNormedZmod_ringType := + [ringType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_comRingType := + [comRingType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_unitRingType := + [unitRingType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_comUnitRingType := + [comUnitRingType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_idomainType := + [idomainType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_fieldType := + [fieldType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_porderType := + [porderType of numField_pseudoMetricNormedZmodType]. +Definition pseudoMetricNormedZmod_numDomainType := + [numDomainType of numField_pseudoMetricNormedZmodType]. +Definition normedMod_ringType := [ringType of numField_normedModType]. +Definition normedMod_comRingType := [comRingType of numField_normedModType]. +Definition normedMod_unitRingType := [unitRingType of numField_normedModType]. +Definition normedMod_comUnitRingType := + [comUnitRingType of numField_normedModType]. +Definition normedMod_idomainType := [idomainType of numField_normedModType]. +Definition normedMod_fieldType := [fieldType of numField_normedModType]. +Definition normedMod_porderType := [porderType of numField_normedModType]. +Definition normedMod_numDomainType := [numDomainType of numField_normedModType]. +End numFieldType. + +Module Exports. +Export topology.nonforgetful_inheritance.Exports. +(* realType *) +Canonical real_lmodType. +Canonical real_lalgType. +Canonical real_algType. +Canonical real_comAlgType. +Canonical real_unitAlgType. +Canonical real_comUnitAlgType. +Canonical real_vectType. +Canonical real_FalgType. +Canonical real_fieldExtType. +Canonical real_pseudoMetricNormedZmodType. +Canonical real_normedModType. +Coercion real_lmodType : realType >-> lmodType. +Coercion real_lalgType : realType >-> lalgType. +Coercion real_algType : realType >-> algType. +Coercion real_comAlgType : realType >-> comAlgType. +Coercion real_unitAlgType : realType >-> unitAlgType. +Coercion real_comUnitAlgType : realType >-> comUnitAlgType. +Coercion real_vectType : realType >-> vectType. +Coercion real_FalgType : realType >-> FalgType. +Coercion real_fieldExtType : realType >-> fieldExtType. +Coercion real_pseudoMetricNormedZmodType : + realType >-> pseudoMetricNormedZmodType. +Coercion real_normedModType : realType >-> normedModType. +(* rcfType *) +Canonical rcf_lmodType. +Canonical rcf_lalgType. +Canonical rcf_algType. +Canonical rcf_comAlgType. +Canonical rcf_unitAlgType. +Canonical rcf_comUnitAlgType. +Canonical rcf_vectType. +Canonical rcf_FalgType. +Canonical rcf_fieldExtType. +Canonical rcf_pseudoMetricNormedZmodType. +Canonical rcf_normedModType. +Coercion rcf_lmodType : rcfType >-> lmodType. +Coercion rcf_lalgType : rcfType >-> lalgType. +Coercion rcf_algType : rcfType >-> algType. +Coercion rcf_comAlgType : rcfType >-> comAlgType. +Coercion rcf_unitAlgType : rcfType >-> unitAlgType. +Coercion rcf_comUnitAlgType : rcfType >-> comUnitAlgType. +Coercion rcf_vectType : rcfType >-> vectType. +Coercion rcf_FalgType : rcfType >-> FalgType. +Coercion rcf_fieldExtType : rcfType >-> fieldExtType. +Coercion rcf_pseudoMetricNormedZmodType : + rcfType >-> pseudoMetricNormedZmodType. +Coercion rcf_normedModType : rcfType >-> normedModType. +(* archiFieldType *) +Canonical archiField_lmodType. +Canonical archiField_lalgType. +Canonical archiField_algType. +Canonical archiField_comAlgType. +Canonical archiField_unitAlgType. +Canonical archiField_comUnitAlgType. +Canonical archiField_vectType. +Canonical archiField_FalgType. +Canonical archiField_fieldExtType. +Canonical archiField_pseudoMetricNormedZmodType. +Canonical archiField_normedModType. +Coercion archiField_lmodType : archiFieldType >-> lmodType. +Coercion archiField_lalgType : archiFieldType >-> lalgType. +Coercion archiField_algType : archiFieldType >-> algType. +Coercion archiField_comAlgType : archiFieldType >-> comAlgType. +Coercion archiField_unitAlgType : archiFieldType >-> unitAlgType. +Coercion archiField_comUnitAlgType : archiFieldType >-> comUnitAlgType. +Coercion archiField_vectType : archiFieldType >-> vectType. +Coercion archiField_FalgType : archiFieldType >-> FalgType. +Coercion archiField_fieldExtType : archiFieldType >-> fieldExtType. +Coercion archiField_pseudoMetricNormedZmodType : + archiFieldType >-> pseudoMetricNormedZmodType. +Coercion archiField_normedModType : archiFieldType >-> normedModType. +(* realFieldType *) +Canonical realField_lmodType. +Canonical realField_lalgType. +Canonical realField_algType. +Canonical realField_comAlgType. +Canonical realField_unitAlgType. +Canonical realField_comUnitAlgType. +Canonical realField_vectType. +Canonical realField_FalgType. +Canonical realField_fieldExtType. +Canonical realField_pseudoMetricNormedZmodType. +Canonical realField_normedModType. +Canonical lmod_latticeType. +Canonical lmod_distrLatticeType. +Canonical lmod_orderType. +Canonical lmod_realDomainType. +Canonical lalg_latticeType. +Canonical lalg_distrLatticeType. +Canonical lalg_orderType. +Canonical lalg_realDomainType. +Canonical alg_latticeType. +Canonical alg_distrLatticeType. +Canonical alg_orderType. +Canonical alg_realDomainType. +Canonical comAlg_latticeType. +Canonical comAlg_distrLatticeType. +Canonical comAlg_orderType. +Canonical comAlg_realDomainType. +Canonical unitAlg_latticeType. +Canonical unitAlg_distrLatticeType. +Canonical unitAlg_orderType. +Canonical unitAlg_realDomainType. +Canonical comUnitAlg_latticeType. +Canonical comUnitAlg_distrLatticeType. +Canonical comUnitAlg_orderType. +Canonical comUnitAlg_realDomainType. +Canonical vect_latticeType. +Canonical vect_distrLatticeType. +Canonical vect_orderType. +Canonical vect_realDomainType. +Canonical Falg_latticeType. +Canonical Falg_distrLatticeType. +Canonical Falg_orderType. +Canonical Falg_realDomainType. +Canonical fieldExt_latticeType. +Canonical fieldExt_distrLatticeType. +Canonical fieldExt_orderType. +Canonical fieldExt_realDomainType. +Canonical pseudoMetricNormedZmod_latticeType. +Canonical pseudoMetricNormedZmod_distrLatticeType. +Canonical pseudoMetricNormedZmod_orderType. +Canonical pseudoMetricNormedZmod_realDomainType. +Canonical normedMod_latticeType. +Canonical normedMod_distrLatticeType. +Canonical normedMod_orderType. +Canonical normedMod_realDomainType. +Coercion realField_lmodType : realFieldType >-> lmodType. +Coercion realField_lalgType : realFieldType >-> lalgType. +Coercion realField_algType : realFieldType >-> algType. +Coercion realField_comAlgType : realFieldType >-> comAlgType. +Coercion realField_unitAlgType : realFieldType >-> unitAlgType. +Coercion realField_comUnitAlgType : realFieldType >-> comUnitAlgType. +Coercion realField_vectType : realFieldType >-> vectType. +Coercion realField_FalgType : realFieldType >-> FalgType. +Coercion realField_fieldExtType : realFieldType >-> fieldExtType. +Coercion realField_pseudoMetricNormedZmodType : + Num.RealField.type >-> PseudoMetricNormedZmodule.type. +Coercion realField_normedModType : Num.RealField.type >-> NormedModule.type. +(* numClosedFieldType *) +Canonical numClosedField_lmodType. +Canonical numClosedField_lalgType. +Canonical numClosedField_algType. +Canonical numClosedField_comAlgType. +Canonical numClosedField_unitAlgType. +Canonical numClosedField_comUnitAlgType. +Canonical numClosedField_vectType. +Canonical numClosedField_FalgType. +Canonical numClosedField_fieldExtType. +Canonical numClosedField_pseudoMetricNormedZmodType. +Canonical numClosedField_normedModType. +Canonical lmod_decFieldType. +Canonical lmod_closedFieldType. +Canonical lalg_decFieldType. +Canonical lalg_closedFieldType. +Canonical alg_decFieldType. +Canonical alg_closedFieldType. +Canonical comAlg_decFieldType. +Canonical comAlg_closedFieldType. +Canonical unitAlg_decFieldType. +Canonical unitAlg_closedFieldType. +Canonical comUnitAlg_decFieldType. +Canonical comUnitAlg_closedFieldType. +Canonical vect_decFieldType. +Canonical vect_closedFieldType. +Canonical Falg_decFieldType. +Canonical Falg_closedFieldType. +Canonical fieldExt_decFieldType. +Canonical fieldExt_closedFieldType. +Canonical pseudoMetricNormedZmod_decFieldType. +Canonical pseudoMetricNormedZmod_closedFieldType. +Canonical normedMod_decFieldType. +Canonical normedMod_closedFieldType. +Coercion numClosedField_lmodType : numClosedFieldType >-> lmodType. +Coercion numClosedField_lalgType : numClosedFieldType >-> lalgType. +Coercion numClosedField_algType : numClosedFieldType >-> algType. +Coercion numClosedField_comAlgType : numClosedFieldType >-> comAlgType. +Coercion numClosedField_unitAlgType : numClosedFieldType >-> unitAlgType. +Coercion numClosedField_comUnitAlgType : numClosedFieldType >-> comUnitAlgType. +Coercion numClosedField_vectType : numClosedFieldType >-> vectType. +Coercion numClosedField_FalgType : numClosedFieldType >-> FalgType. +Coercion numClosedField_fieldExtType : numClosedFieldType >-> fieldExtType. +Coercion numClosedField_pseudoMetricNormedZmodType : + numClosedFieldType >-> pseudoMetricNormedZmodType. +Coercion numClosedField_normedModType : numClosedFieldType >-> normedModType. +(* numFieldType *) +Canonical numField_lmodType. +Canonical numField_lalgType. +Canonical numField_algType. +Canonical numField_comAlgType. +Canonical numField_unitAlgType. +Canonical numField_comUnitAlgType. +Canonical numField_vectType. +Canonical numField_FalgType. +Canonical numField_fieldExtType. +Canonical numField_pseudoMetricNormedZmodType. +Canonical numField_normedModType. +Canonical lmod_porderType. +Canonical lmod_numDomainType. +Canonical lalg_pointedType. +Canonical lalg_filteredType. +Canonical lalg_topologicalType. +Canonical lalg_uniformType. +Canonical lalg_pseudoMetricType. +Canonical lalg_normedZmodType. +Canonical lalg_pseudoMetricNormedZmodType. +Canonical lalg_normedModType. +Canonical lalg_porderType. +Canonical lalg_numDomainType. +Canonical alg_pointedType. +Canonical alg_filteredType. +Canonical alg_topologicalType. +Canonical alg_uniformType. +Canonical alg_pseudoMetricType. +Canonical alg_normedZmodType. +Canonical alg_pseudoMetricNormedZmodType. +Canonical alg_normedModType. +Canonical alg_porderType. +Canonical alg_numDomainType. +Canonical comAlg_pointedType. +Canonical comAlg_filteredType. +Canonical comAlg_topologicalType. +Canonical comAlg_uniformType. +Canonical comAlg_pseudoMetricType. +Canonical comAlg_normedZmodType. +Canonical comAlg_pseudoMetricNormedZmodType. +Canonical comAlg_normedModType. +Canonical comAlg_porderType. +Canonical comAlg_numDomainType. +Canonical unitAlg_pointedType. +Canonical unitAlg_filteredType. +Canonical unitAlg_topologicalType. +Canonical unitAlg_uniformType. +Canonical unitAlg_pseudoMetricType. +Canonical unitAlg_normedZmodType. +Canonical unitAlg_pseudoMetricNormedZmodType. +Canonical unitAlg_normedModType. +Canonical unitAlg_porderType. +Canonical unitAlg_numDomainType. +Canonical comUnitAlg_pointedType. +Canonical comUnitAlg_filteredType. +Canonical comUnitAlg_topologicalType. +Canonical comUnitAlg_uniformType. +Canonical comUnitAlg_pseudoMetricType. +Canonical comUnitAlg_normedZmodType. +Canonical comUnitAlg_pseudoMetricNormedZmodType. +Canonical comUnitAlg_normedModType. +Canonical comUnitAlg_porderType. +Canonical comUnitAlg_numDomainType. +Canonical vect_pointedType. +Canonical vect_filteredType. +Canonical vect_topologicalType. +Canonical vect_uniformType. +Canonical vect_pseudoMetricType. +Canonical vect_normedZmodType. +Canonical vect_pseudoMetricNormedZmodType. +Canonical vect_normedModType. +Canonical vect_porderType. +Canonical vect_numDomainType. +Canonical Falg_pointedType. +Canonical Falg_filteredType. +Canonical Falg_topologicalType. +Canonical Falg_uniformType. +Canonical Falg_pseudoMetricType. +Canonical Falg_normedZmodType. +Canonical Falg_pseudoMetricNormedZmodType. +Canonical Falg_normedModType. +Canonical Falg_porderType. +Canonical Falg_numDomainType. +Canonical fieldExt_pointedType. +Canonical fieldExt_filteredType. +Canonical fieldExt_topologicalType. +Canonical fieldExt_uniformType. +Canonical fieldExt_pseudoMetricType. +Canonical fieldExt_normedZmodType. +Canonical fieldExt_pseudoMetricNormedZmodType. +Canonical fieldExt_normedModType. +Canonical fieldExt_porderType. +Canonical fieldExt_numDomainType. +Canonical pseudoMetricNormedZmod_ringType. +Canonical pseudoMetricNormedZmod_comRingType. +Canonical pseudoMetricNormedZmod_unitRingType. +Canonical pseudoMetricNormedZmod_comUnitRingType. +Canonical pseudoMetricNormedZmod_idomainType. +Canonical pseudoMetricNormedZmod_fieldType. +Canonical pseudoMetricNormedZmod_porderType. +Canonical pseudoMetricNormedZmod_numDomainType. +Canonical normedMod_ringType. +Canonical normedMod_comRingType. +Canonical normedMod_unitRingType. +Canonical normedMod_comUnitRingType. +Canonical normedMod_idomainType. +Canonical normedMod_fieldType. +Canonical normedMod_porderType. +Canonical normedMod_numDomainType. +Coercion numField_lmodType : numFieldType >-> lmodType. +Coercion numField_lalgType : numFieldType >-> lalgType. +Coercion numField_algType : numFieldType >-> algType. +Coercion numField_comAlgType : numFieldType >-> comAlgType. +Coercion numField_unitAlgType : numFieldType >-> unitAlgType. +Coercion numField_comUnitAlgType : numFieldType >-> comUnitAlgType. +Coercion numField_vectType : numFieldType >-> vectType. +Coercion numField_FalgType : numFieldType >-> FalgType. +Coercion numField_fieldExtType : numFieldType >-> fieldExtType. +Coercion numField_pseudoMetricNormedZmodType : + numFieldType >-> pseudoMetricNormedZmodType. +Coercion numField_normedModType : numFieldType >-> normedModType. +End Exports. +End nonforgetful_inheritance. +Import nonforgetful_inheritance.Exports. Section NormedModule_numDomainType. Variables (R : numDomainType) (V : normedModType R). @@ -2157,7 +2423,7 @@ by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP. Qed. Lemma cvg_norm f a : f @ F --> a -> `|f x| @[x --> F] --> (`|a| : K). -Proof. exact: (continuous_cvg _ (@norm_continuous _ _ _)). Qed. +Proof. by apply: continuous_cvg; apply: norm_continuous. Qed. Lemma is_cvg_norm f : cvg (f @ F) -> cvg ((Num.norm \o f : T -> K) @ F). Proof. by have := cvgP _ (cvg_norm _); apply. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 4d3db2f900..a8e17cca2a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -48,6 +48,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import nonforgetful_inheritance.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -476,7 +477,7 @@ Proof. by rewrite /= invr_gt0 ltr0n. Qed. Lemma harmonic_ge0 {R : numFieldType} i : 0 <= harmonic i :> R. Proof. exact/ltW/harmonic_gt0. Qed. -Lemma cvg_harmonic {R : archiFieldType} : (@harmonic R) --> (0 : R). +Lemma cvg_harmonic {R : archiFieldType} : harmonic --> (0 : R). Proof. apply: cvg_distW => _/posnumP[e]; rewrite near_map; near=> i. rewrite distrC subr0 ger0_norm//= -lef_pinv ?qualifE// invrK. @@ -551,8 +552,7 @@ by rewrite lef_pinv // ?ler_nat // posrE // ltr0n. Grab Existential Variables. all: end_near. Qed. Lemma cesaro_converse (u_ : R ^nat) (l : R) : - telescope u_ =o_\oo (@harmonic R) -> - arithmetic_mean u_ --> l -> u_ --> l. + telescope u_ =o_\oo harmonic -> arithmetic_mean u_ --> l -> u_ --> l. Proof. pose a_ := telescope u_ => a_o u_l. suff abel : forall n, @@ -572,12 +572,12 @@ suff abel : forall n, have {}a_o : [sequence n.+1%:R * telescope u_ n]_n --> (0 : R). apply: (@eqolim0 _ _ _ eventually_filterType). rewrite a_o. - set h := 'o_[filter of \oo] (@harmonic R). + set h := 'o_[filter of \oo] harmonic. apply/eqoP => _/posnumP[e] /=. near=> n; rewrite normr1 mulr1 normrM -ler_pdivl_mull ?normr_gt0 //. rewrite mulrC -normrV ?unitfE //. near: n. - by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh. + by case: (eqoP eventually_filterType harmonic h) => Hh _; apply Hh. move: (cesaro a_o); rewrite /arithmetic_mean /series /= -/a_. exact: (@cesaro_converse_off_by_one (fun k : nat => k.+1%:R * a_ k)). case => [|n]. diff --git a/theories/topology.v b/theories/topology.v index 9f3e51ccdf..54986c5abc 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3896,7 +3896,6 @@ by rewrite inE => /orP [/eqP->|/ihl leminlfi]; rewrite le_minl ?lexx // leminlfi orbC. Qed. -Canonical R_pointedType := PointedType R 0. Lemma mx_entourage : entourage = entourage_ mx_ball. Proof. rewrite predeqE=> A; split; last first. @@ -4307,13 +4306,13 @@ Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K) Section pseudoMetric_of_normedDomain. Variables (K : numDomainType) (R : normedZmodType K). -Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.Def.normr x e x. +Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.norm x e x. Proof. by move=> ? /=; rewrite subrr normr0. Qed. Lemma ball_norm_symmetric (x y : R) (e : K) : - ball_ Num.Def.normr x e y -> ball_ Num.Def.normr y e x. + ball_ Num.norm x e y -> ball_ Num.norm y e x. Proof. by rewrite /= distrC. Qed. Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) : - ball_ Num.Def.normr x e1 y -> ball_ Num.Def.normr y e2 z -> ball_ Num.Def.normr x (e1 + e2) z. + ball_ Num.norm x e1 y -> ball_ Num.norm y e2 z -> ball_ Num.norm x (e1 + e2) z. Proof. move=> /= ? ?; rewrite -(subr0 x) -(subrr y) opprD opprK (addrA x _ y) -addrA. by rewrite (le_lt_trans (ler_norm_add _ _)) // ltr_add. @@ -4322,207 +4321,367 @@ Definition pseudoMetric_of_normedDomain : PseudoMetric.mixin_of K (@entourage_ K R R (ball_ (fun x => `|x|))) := PseudoMetricMixin ball_norm_center ball_norm_symmetric ball_norm_triangle erefl. Lemma nbhs_ball_normE : - @nbhs_ball_ K R R (ball_ Num.Def.normr) = nbhs_ (entourage_ (ball_ Num.Def.normr)). + @nbhs_ball_ K R R (ball_ Num.norm) = nbhs_ (entourage_ (ball_ Num.norm)). Proof. rewrite /nbhs_ entourage_E predeq2E => x A; split. move=> [e egt0 sbeA]. - by exists [set xy | ball_ Num.Def.normr xy.1 e xy.2] => //; exists e. + by exists [set xy | ball_ Num.norm xy.1 e xy.2] => //; exists e. by move=> [E [e egt0 sbeE] sEA]; exists e => // ??; apply/sEA/sbeE. Qed. End pseudoMetric_of_normedDomain. -Section numFieldType_canonical. - -Canonical numFieldType_pointedType (R: numFieldType) := - [pointedType of R for pointed_of_zmodule R]. -Canonical numFieldType_filteredType (R: numFieldType) := - [filteredType R of R for filtered_of_normedZmod R]. -Canonical numFieldType_topologicalType (R: numFieldType) : topologicalType := - TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical numFieldType_uniformType (R: numFieldType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical numFieldType_pseudoMetricType (R: numFieldType) - := @PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). -(* (*NEW*) *) - -Canonical numClosedFieldType_pointedType (R: numClosedFieldType) := - [pointedType of R for [pointedType of [numFieldType of R]]]. -Canonical numClosedFieldType_filteredType (R: numClosedFieldType) := - [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. -Canonical numClosedFieldType_topologicalType (R: numClosedFieldType) : topologicalType := - (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) - (*leads to ambiguous path *) - TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical numClosedFieldType_uniformType (R: numClosedFieldType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical numClosedFieldType_pseudoMetricType (R: numClosedFieldType) := - (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) - (* leads to ambiguous path *) - @PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). - -Canonical realFieldType_pointedType (R: realFieldType) := - [pointedType of R for [pointedType of [numFieldType of R]]]. -Canonical realFieldType_filteredType (R: realFieldType) := - [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. -Canonical realFieldType_topologicalType (R: realFieldType) : topologicalType := - (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) - (*leads to ambiguous path *) - TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical realFieldType_uniformType (R: realFieldType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical realFieldType_pseudoMetricType (R: realFieldType) := - (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) - (* leads to ambiguous path *) - @PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). - -Canonical archiFieldType_pointedType (R: archiFieldType) := - [pointedType of R for [pointedType of [numFieldType of R]]]. -Canonical archiFieldType_filteredType (R: archiFieldType) := - [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. -Canonical archiFieldType_topologicalType (R: archiFieldType) : topologicalType := - (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) - (*leads to ambiguous path *) - TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical archiFieldType_uniformType (R: archiFieldType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical archiFieldType_pseudoMetricType (R: archiFieldType):= - (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) - (* leads to ambiguous path *) - @PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). - -Canonical rcfType_pointedType (R: rcfType) := - [pointedType of R for [pointedType of [numFieldType of R]]]. -Canonical rcfType_filteredType (R: rcfType) := - [filteredType R of R for filtered_of_normedZmod R]. -Canonical rcfType_topologicalType (R: rcfType) : topologicalType := - (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) - (*leads to ambiguous path *) -TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical rcfType_uniformType (R: rcfType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical rcfType_pseudoMetricType (R: rcfType) := - (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) - (* leads to ambiguous path *) - @PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). - -Canonical realType_pointedType (R: realType) := - [pointedType of R for [pointedType of [numFieldType of R]]]. -Canonical realType_filteredType (R: realType) := - [filteredType _ of R for [filteredType _ of [numFieldType of R]]]. -Canonical realType_topologicalType (R: realType) : topologicalType := - (* [topologicalType of R for [topologicalType of [numFieldType of R]]]. *) - (*leads to ambiguous path *) - TopologicalType R - (topologyOfEntourageMixin - (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical realType_uniformType (R: realType) : uniformType := UniformType R - (uniformityOfBallMixin (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical realType_pseudoMetricType (R: realType) := - (* [pseudoMetricType _ of R for [pseudoMetricType _ of [numFieldType of R]]]. *) - (* leads to ambiguous path *) -@PseudoMetric.Pack R R (@PseudoMetric.Class R R - (Uniform.class (numFieldType_uniformType R)) (@pseudoMetric_of_normedDomain R R)). - -Coercion numFieldType_pointedType : numFieldType >-> pointedType. -Coercion numFieldType_filteredType : numFieldType >-> filteredType. -Coercion numFieldType_topologicalType : numFieldType >-> topologicalType. -Coercion numFieldType_uniformType : numFieldType >-> uniformType. -Coercion numFieldType_pseudoMetricType : numFieldType >-> pseudoMetricType. - -Coercion numClosedFieldType_pointedType : numClosedFieldType >-> pointedType. -Coercion numClosedFieldType_filteredType : numClosedFieldType >-> filteredType. -Coercion numClosedFieldType_topologicalType : numClosedFieldType >-> topologicalType. -Coercion numClosedFieldType_uniformType : numClosedFieldType >-> uniformType. -Coercion numClosedFieldType_pseudoMetricType : numClosedFieldType >-> pseudoMetricType. - -Coercion realFieldType_pointedType : realFieldType >-> pointedType. -Coercion realFieldType_filteredType : realFieldType >-> filteredType. -Coercion realFieldType_topologicalType : realFieldType >-> topologicalType. -Coercion realFieldType_uniformType : realFieldType >-> uniformType. -Coercion realFieldType_pseudoMetricType : realFieldType >-> pseudoMetricType. - -Coercion archiFieldType_pointedType : archiFieldType >-> pointedType. -Coercion archiFieldType_filteredType : archiFieldType >-> filteredType. -Coercion archiFieldType_topologicalType : archiFieldType >-> topologicalType. -Coercion archiFieldType_uniformType : archiFieldType >-> uniformType. -Coercion archiFieldType_pseudoMetricType : archiFieldType >-> pseudoMetricType. - -Coercion rcfType_pointedType : rcfType >-> pointedType. -Coercion rcfType_filteredType : rcfType >-> filteredType. -Coercion rcfType_topologicalType : rcfType >-> topologicalType. -Coercion rcfType_uniformType : rcfType >-> uniformType. -Coercion rcfType_pseudoMetricType : rcfType >-> pseudoMetricType. - -Coercion realType_pointedType : realType >-> pointedType. -Coercion realType_filteredType : realType >-> filteredType. -Coercion realType_topologicalType : realType >-> topologicalType. -Coercion realType_uniformType : realType >-> uniformType. -Coercion realType_pseudoMetricType : realType >-> pseudoMetricType. - - -Definition numFieldType_lalgType (R : numFieldType) : lalgType R := - @GRing.regular_lalgType R. - -End numFieldType_canonical. - - - -Module numFieldType_regular_canonical. - -Canonical numFieldType_regular_pointedType (R : numFieldType) := +Module regular_topology. + +Section regular_topology. +Local Canonical pointedType (R : zmodType) : pointedType := [pointedType of R^o for pointed_of_zmodule R]. -Canonical numFieldType_regular_filteredType (R : numFieldType) := +Local Canonical filteredType (R : numDomainType) : filteredType R := [filteredType R of R^o for filtered_of_normedZmod R]. -Canonical numFieldType_regular_topologicalType (R : numFieldType) : topologicalType := - TopologicalType R^o (topologyOfEntourageMixin (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R]))). -Canonical numFieldType_regular_uniformType (R : numFieldType) : uniformType := +Local Canonical topologicalType (R : numFieldType) : topologicalType := + TopologicalType R^o (topologyOfEntourageMixin (uniformityOfBallMixin + (@nbhs_ball_normE _ _) (pseudoMetric_of_normedDomain _))). +Local Canonical uniformType (R : numFieldType) : uniformType := UniformType R^o (uniformityOfBallMixin - (@nbhs_ball_normE _ [normedZmodType R of R]) - (pseudoMetric_of_normedDomain [normedZmodType R of R])). -Canonical numFieldType_regular_pseudoMetricType (R : numFieldType) := - @PseudoMetric.Pack R R^o (@PseudoMetric.Class R R - (Uniform.class (numFieldType_regular_uniformType R)) (@pseudoMetric_of_normedDomain R R)). + (@nbhs_ball_normE _ _) (pseudoMetric_of_normedDomain _)). +Local Canonical pseudoMetricType (R : numFieldType) := + PseudoMetricType R^o (@pseudoMetric_of_normedDomain R R). +End regular_topology. + +Module Exports. +Canonical pointedType. +Canonical filteredType. +Canonical topologicalType. +Canonical uniformType. +Canonical pseudoMetricType. +End Exports. +End regular_topology. +Export regular_topology.Exports. + +Module nonforgetful_inheritance. + +Section realType. +Variable (R : realType). +Local Canonical real_pointedType := [pointedType of R for [pointedType of R^o]]. +Local Canonical real_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical real_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical real_uniformType := [uniformType of R for [uniformType of R^o]]. +Local Canonical real_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +End realType. + +Section rcfType. +Variable (R : rcfType). +Local Canonical rcf_pointedType := [pointedType of R for [pointedType of R^o]]. +Local Canonical rcf_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical rcf_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical rcf_uniformType := [uniformType of R for [uniformType of R^o]]. +Local Canonical rcf_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +End rcfType. + +Section archiFieldType. +Variable (R : archiFieldType). +Local Canonical archiField_pointedType := + [pointedType of R for [pointedType of R^o]]. +Local Canonical archiField_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical archiField_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical archiField_uniformType := + [uniformType of R for [uniformType of R^o]]. +Local Canonical archiField_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +End archiFieldType. + +Section realFieldType. +Variable (R : realFieldType). +Local Canonical realField_pointedType := + [pointedType of R for [pointedType of R^o]]. +Local Canonical realField_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical realField_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical realField_uniformType := + [uniformType of R for [uniformType of R^o]]. +Local Canonical realField_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +Definition pointed_latticeType := [latticeType of realField_pointedType]. +Definition pointed_distrLatticeType := + [distrLatticeType of realField_pointedType]. +Definition pointed_orderType := [orderType of realField_pointedType]. +Definition pointed_realDomainType := + [realDomainType of realField_pointedType]. +Definition filtered_latticeType := [latticeType of realField_filteredType]. +Definition filtered_distrLatticeType := + [distrLatticeType of realField_filteredType]. +Definition filtered_orderType := [orderType of realField_filteredType]. +Definition filtered_realDomainType := + [realDomainType of realField_filteredType]. +Definition topological_latticeType := + [latticeType of realField_topologicalType]. +Definition topological_distrLatticeType := + [distrLatticeType of realField_topologicalType]. +Definition topological_orderType := [orderType of realField_topologicalType]. +Definition topological_realDomainType := + [realDomainType of realField_topologicalType]. +Definition uniform_latticeType := [latticeType of realField_uniformType]. +Definition uniform_distrLatticeType := + [distrLatticeType of realField_uniformType]. +Definition uniform_orderType := [orderType of realField_uniformType]. +Definition uniform_realDomainType := [realDomainType of realField_uniformType]. +Definition pseudoMetric_latticeType := + [latticeType of realField_pseudoMetricType]. +Definition pseudoMetric_distrLatticeType := + [distrLatticeType of realField_pseudoMetricType]. +Definition pseudoMetric_orderType := [orderType of realField_pseudoMetricType]. +Definition pseudoMetric_realDomainType := + [realDomainType of realField_pseudoMetricType]. +End realFieldType. + +Section numClosedFieldType. +Variable (R : numClosedFieldType). +Local Canonical numClosedField_pointedType := + [pointedType of R for [pointedType of R^o]]. +Local Canonical numClosedField_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical numClosedField_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical numClosedField_uniformType := + [uniformType of R for [uniformType of R^o]]. +Local Canonical numClosedField_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +Definition pointed_decFieldType := + [decFieldType of numClosedField_pointedType]. +Definition pointed_closedFieldType := + [closedFieldType of numClosedField_pointedType]. +Definition filtered_decFieldType := + [decFieldType of numClosedField_filteredType]. +Definition filtered_closedFieldType := + [closedFieldType of numClosedField_filteredType]. +Definition topological_decFieldType := + [decFieldType of numClosedField_topologicalType]. +Definition topological_closedFieldType := + [closedFieldType of numClosedField_topologicalType]. +Definition uniform_decFieldType := [decFieldType of numClosedField_uniformType]. +Definition uniform_closedFieldType := + [closedFieldType of numClosedField_uniformType]. +Definition pseudoMetric_decFieldType := + [decFieldType of numClosedField_pseudoMetricType]. +Definition pseudoMetric_closedFieldType := + [closedFieldType of numClosedField_pseudoMetricType]. +End numClosedFieldType. + +Section numFieldType. +Variable (R : numFieldType). +Local Canonical numField_pointedType := + [pointedType of R for [pointedType of R^o]]. +Local Canonical numField_filteredType := + [filteredType R of R for [filteredType R of R^o]]. +Local Canonical numField_topologicalType := + [topologicalType of R for [topologicalType of R^o]]. +Local Canonical numField_uniformType := + [uniformType of R for [uniformType of R^o]]. +Local Canonical numField_pseudoMetricType := + [pseudoMetricType R of R for [pseudoMetricType R of R^o]]. +Definition pointed_ringType := [ringType of numField_pointedType]. +Definition pointed_comRingType := [comRingType of numField_pointedType]. +Definition pointed_unitRingType := [unitRingType of numField_pointedType]. +Definition pointed_comUnitRingType := [comUnitRingType of numField_pointedType]. +Definition pointed_idomainType := [idomainType of numField_pointedType]. +Definition pointed_fieldType := [fieldType of numField_pointedType]. +Definition pointed_porderType := [porderType of numField_pointedType]. +Definition pointed_numDomainType := [numDomainType of numField_pointedType]. +Definition filtered_ringType := [ringType of numField_filteredType]. +Definition filtered_comRingType := [comRingType of numField_filteredType]. +Definition filtered_unitRingType := [unitRingType of numField_filteredType]. +Definition filtered_comUnitRingType := + [comUnitRingType of numField_filteredType]. +Definition filtered_idomainType := [idomainType of numField_filteredType]. +Definition filtered_fieldType := [fieldType of numField_filteredType]. +Definition filtered_porderType := [porderType of numField_filteredType]. +Definition filtered_numDomainType := [numDomainType of numField_filteredType]. +Definition topological_ringType := [ringType of numField_topologicalType]. +Definition topological_comRingType := [comRingType of numField_topologicalType]. +Definition topological_unitRingType := + [unitRingType of numField_topologicalType]. +Definition topological_comUnitRingType := + [comUnitRingType of numField_topologicalType]. +Definition topological_idomainType := [idomainType of numField_topologicalType]. +Definition topological_fieldType := [fieldType of numField_topologicalType]. +Definition topological_porderType := [porderType of numField_topologicalType]. +Definition topological_numDomainType := + [numDomainType of numField_topologicalType]. +Definition uniform_ringType := [ringType of numField_uniformType]. +Definition uniform_comRingType := [comRingType of numField_uniformType]. +Definition uniform_unitRingType := [unitRingType of numField_uniformType]. +Definition uniform_comUnitRingType := [comUnitRingType of numField_uniformType]. +Definition uniform_idomainType := [idomainType of numField_uniformType]. +Definition uniform_fieldType := [fieldType of numField_uniformType]. +Definition uniform_porderType := [porderType of numField_uniformType]. +Definition uniform_numDomainType := [numDomainType of numField_uniformType]. +Definition pseudoMetric_ringType := [ringType of numField_pseudoMetricType]. +Definition pseudoMetric_comRingType := + [comRingType of numField_pseudoMetricType]. +Definition pseudoMetric_unitRingType := + [unitRingType of numField_pseudoMetricType]. +Definition pseudoMetric_comUnitRingType := + [comUnitRingType of numField_pseudoMetricType]. +Definition pseudoMetric_idomainType := + [idomainType of numField_pseudoMetricType]. +Definition pseudoMetric_fieldType := [fieldType of numField_pseudoMetricType]. +Definition pseudoMetric_porderType := [porderType of numField_pseudoMetricType]. +Definition pseudoMetric_numDomainType := + [numDomainType of numField_pseudoMetricType]. +End numFieldType. -Definition numFieldType_regular_lalgType (R : numFieldType) : lalgType R := - @GRing.regular_lalgType R. +Module Exports. +(* realType *) +Canonical real_pointedType. +Canonical real_filteredType. +Canonical real_topologicalType. +Canonical real_uniformType. +Canonical real_pseudoMetricType. +Coercion real_pointedType : realType >-> pointedType. +Coercion real_filteredType : realType >-> filteredType. +Coercion real_topologicalType : realType >-> topologicalType. +Coercion real_uniformType : realType >-> uniformType. +Coercion real_pseudoMetricType : realType >-> pseudoMetricType. +(* rcfType *) +Canonical rcf_pointedType. +Canonical rcf_filteredType. +Canonical rcf_topologicalType. +Canonical rcf_uniformType. +Canonical rcf_pseudoMetricType. +Coercion rcf_pointedType : rcfType >-> pointedType. +Coercion rcf_filteredType : rcfType >-> filteredType. +Coercion rcf_topologicalType : rcfType >-> topologicalType. +Coercion rcf_uniformType : rcfType >-> uniformType. +Coercion rcf_pseudoMetricType : rcfType >-> pseudoMetricType. +(* archiFieldType *) +Canonical archiField_pointedType. +Canonical archiField_filteredType. +Canonical archiField_topologicalType. +Canonical archiField_uniformType. +Canonical archiField_pseudoMetricType. +Coercion archiField_pointedType : archiFieldType >-> pointedType. +Coercion archiField_filteredType : archiFieldType >-> filteredType. +Coercion archiField_topologicalType : archiFieldType >-> topologicalType. +Coercion archiField_uniformType : archiFieldType >-> uniformType. +Coercion archiField_pseudoMetricType : archiFieldType >-> pseudoMetricType. +(* realFieldType *) +Canonical realField_pointedType. +Canonical realField_filteredType. +Canonical realField_topologicalType. +Canonical realField_uniformType. +Canonical realField_pseudoMetricType. +Canonical pointed_latticeType. +Canonical pointed_distrLatticeType. +Canonical pointed_orderType. +Canonical pointed_realDomainType. +Canonical filtered_latticeType. +Canonical filtered_distrLatticeType. +Canonical filtered_orderType. +Canonical filtered_realDomainType. +Canonical topological_latticeType. +Canonical topological_distrLatticeType. +Canonical topological_orderType. +Canonical topological_realDomainType. +Canonical uniform_latticeType. +Canonical uniform_distrLatticeType. +Canonical uniform_orderType. +Canonical uniform_realDomainType. +Canonical pseudoMetric_latticeType. +Canonical pseudoMetric_distrLatticeType. +Canonical pseudoMetric_orderType. +Canonical pseudoMetric_realDomainType. +Coercion realField_pointedType : realFieldType >-> pointedType. +Coercion realField_filteredType : realFieldType >-> filteredType. +Coercion realField_topologicalType : realFieldType >-> topologicalType. +Coercion realField_uniformType : realFieldType >-> uniformType. +Coercion realField_pseudoMetricType : realFieldType >-> pseudoMetricType. +(* numClosedFieldType *) +Canonical numClosedField_pointedType. +Canonical numClosedField_filteredType. +Canonical numClosedField_topologicalType. +Canonical numClosedField_uniformType. +Canonical numClosedField_pseudoMetricType. +Canonical pointed_decFieldType. +Canonical pointed_closedFieldType. +Canonical filtered_decFieldType. +Canonical filtered_closedFieldType. +Canonical topological_decFieldType. +Canonical topological_closedFieldType. +Canonical uniform_decFieldType. +Canonical uniform_closedFieldType. +Canonical pseudoMetric_decFieldType. +Canonical pseudoMetric_closedFieldType. +Coercion numClosedField_pointedType : numClosedFieldType >-> pointedType. +Coercion numClosedField_filteredType : numClosedFieldType >-> filteredType. +Coercion numClosedField_topologicalType : + numClosedFieldType >-> topologicalType. +Coercion numClosedField_uniformType : numClosedFieldType >-> uniformType. +Coercion numClosedField_pseudoMetricType : + numClosedFieldType >-> pseudoMetricType. +(* numFieldType *) +Canonical numField_pointedType. +Canonical numField_filteredType. +Canonical numField_topologicalType. +Canonical numField_uniformType. +Canonical numField_pseudoMetricType. +Canonical pointed_ringType. +Canonical pointed_comRingType. +Canonical pointed_unitRingType. +Canonical pointed_comUnitRingType. +Canonical pointed_idomainType. +Canonical pointed_fieldType. +Canonical pointed_porderType. +Canonical pointed_numDomainType. +Canonical filtered_ringType. +Canonical filtered_comRingType. +Canonical filtered_unitRingType. +Canonical filtered_comUnitRingType. +Canonical filtered_idomainType. +Canonical filtered_fieldType. +Canonical filtered_porderType. +Canonical filtered_numDomainType. +Canonical topological_ringType. +Canonical topological_comRingType. +Canonical topological_unitRingType. +Canonical topological_comUnitRingType. +Canonical topological_idomainType. +Canonical topological_fieldType. +Canonical topological_porderType. +Canonical topological_numDomainType. +Canonical uniform_ringType. +Canonical uniform_comRingType. +Canonical uniform_unitRingType. +Canonical uniform_comUnitRingType. +Canonical uniform_idomainType. +Canonical uniform_fieldType. +Canonical uniform_porderType. +Canonical uniform_numDomainType. +Canonical pseudoMetric_ringType. +Canonical pseudoMetric_comRingType. +Canonical pseudoMetric_unitRingType. +Canonical pseudoMetric_comUnitRingType. +Canonical pseudoMetric_idomainType. +Canonical pseudoMetric_fieldType. +Canonical pseudoMetric_porderType. +Canonical pseudoMetric_numDomainType. +Coercion numField_pointedType : numFieldType >-> pointedType. +Coercion numField_filteredType : numFieldType >-> filteredType. +Coercion numField_topologicalType : numFieldType >-> topologicalType. +Coercion numField_uniformType : numFieldType >-> uniformType. +Coercion numField_pseudoMetricType : numFieldType >-> pseudoMetricType. +End Exports. -End numFieldType_regular_canonical. +End nonforgetful_inheritance. +Import nonforgetful_inheritance.Exports. Global Instance Proper_nbhs'_regular_numFieldType (R : numFieldType) (x : R^o) : ProperFilter (nbhs' x). @@ -4534,7 +4693,6 @@ rewrite /ball /= opprD addrA subrr distrC subr0 ger0_norm //. by rewrite {2}(splitr e%:num) ltr_spaddl. Qed. - Global Instance Proper_nbhs'_numFieldType (R : numFieldType) (x : R) : ProperFilter (nbhs' x). Proof.