From 1e86da1e1ddfe1f660483eed4fee0873f6e339e3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 3 Apr 2026 16:33:13 +0900 Subject: [PATCH] test subNormedZmodType --- .../pseudometric_normed_Zmodule.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 626f3296f..2b4f5f0b9 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -143,6 +143,22 @@ HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) := {T of Num.NormedZmodule R T & PseudoMetric R T & NormedZmod_PseudoMetric_eq R T & isPointed T}. +HB.mixin Record Zmodule_isSubSemiNormed (R : numDomainType) + (M : semiNormedZmodType R) (S : pred M) T & SubType M S T + & Num.NormedZmodule R T := { + norm_valE : @Num.norm _ M \o (val : T -> M) = @Num.norm _ T +}. + +#[short(type="subSemiNormedZmodType")] +HB.structure Definition SubSemiNormedZmodule (R : numDomainType) + (V : semiNormedZmodType R) (S : pred V) := + { W of GRing.SubZmodule V S W & Zmodule_isSubSemiNormed R V S W}. + +#[short(type="subNormedZmodType")] +HB.structure Definition SubNormedZmodule (R : numDomainType) + (V : normedZmodType R) (S : pred V) := + { U of SubChoice V S U & Num.NormedZmodule R U & @SubSemiNormedZmodule R V S U }. + (* alternative definition of a PseudoMetricNormedZmod *) HB.factory Record NormedZmoduleMetric (R : numDomainType) T & Num.NormedZmodule R T & Metric R T & isPointed T := {