From f34ace87ab707b4781390968d4d3a34ce937fba8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 6 Sep 2024 14:00:10 +0900 Subject: [PATCH] fixes #1308 --- theories/numfun.v | 4 ---- 1 file changed, 4 deletions(-) diff --git a/theories/numfun.v b/theories/numfun.v index a6e98d544..ce6d63bab 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -469,8 +469,6 @@ HB.end. Section Tietze. Context {X : topologicalType} {R : realType}. -Local Notation "3" := 3%:R : ring_scope. - Hypothesis normalX : normal_space X. Lemma urysohn_ext_itv A B x y : @@ -495,8 +493,6 @@ Qed. Context (A : set X). Hypothesis clA : closed A. -Local Notation "3" := 3%:R. - Local Lemma tietze_step' (f : X -> R) (M : R) : 0 < M -> {within A, continuous f} -> (forall x, A x -> `|f x| <= M) ->