From 5e7ea5704b4a6eb86e3c1936eff64c513abd633a Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 19 Nov 2024 14:37:20 +0100 Subject: [PATCH] adapt to mc#19611 --- theories/tvs.v | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/theories/tvs.v b/theories/tvs.v index 564e20036..37cc7ff65 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -124,18 +124,16 @@ Definition entourage : set_system (E * E) := (forall xy : E * E, (xy.1 - xy.2) \in U -> xy \in P). Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U). -Proof. by apply: nbhs0N_subproof; exact: scale_continuous. Qed. +Proof. by apply: (@nbhs0N_subproof _ _ (GRing.Lmodule.class E)); exact: scale_continuous. Qed. Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U). -Proof. -by apply: nbhsN_subproof; exact: scale_continuous. -Qed. +Proof. by apply: (@nbhsN_subproof _ _ (GRing.Lmodule.class E)); exact: scale_continuous. Qed. Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U). -Proof. by apply: nbhsT_subproof; exact: add_continuous. Qed. +Proof. by apply: (@nbhsT_subproof _ _ (GRing.Lmodule.class E)); exact: add_continuous. Qed. Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U). -Proof. by apply: nbhsB_subproof; exact: add_continuous. Qed. +Proof. by apply: (@nbhsB_subproof _ _ (GRing.Lmodule.class E)); exact: add_continuous. Qed. Lemma entourage_filter : Filter entourage. Proof. @@ -216,13 +214,13 @@ Section Tvs_numDomain. Context (R : numDomainType) (E : tvsType R) (U : set E). Lemma nbhs0N : nbhs 0 U -> nbhs 0 (-%R @` U). -Proof. exact/nbhs0N_subproof/scale_continuous. Qed. +Proof. exact/(@nbhs0N_subproof _ _ (GRing.Lmodule.class E))/scale_continuous. Qed. Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U). -Proof. exact/nbhsT_subproof/add_continuous. Qed. +Proof. exact/(@nbhsT_subproof _ _ (GRing.Lmodule.class E))/add_continuous. Qed. Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U). -Proof. exact/nbhsB_subproof/add_continuous. Qed. +Proof. exact/(@nbhsB_subproof _ _ (GRing.Lmodule.class E))/add_continuous. Qed. End Tvs_numDomain.