From 7bd28f69e151db4bce970a21b5c81a595e57c590 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 17 May 2026 10:05:26 +0900 Subject: [PATCH] fix issue #1973 --- theories/normedtype_theory/tvs.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 00b1a33851..c578687637 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -525,6 +525,14 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E entourage_filter entourage_refl entourage_inv entourage_split_ex nbhsE. + + +HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous. + +HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous. + +HB.instance Definition _ := Uniform_isConvexTvs.Build R E locally_convex. + HB.end. Section ConvexTvs_numDomain.