From 610cc328de8b12ff9056cea3365fde09414d2681 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 4 Oct 2024 10:55:29 -0400 Subject: [PATCH] removing unused lemma --- CHANGELOG_UNRELEASED.md | 4 ++-- theories/normedtype.v | 15 +-------------- 2 files changed, 3 insertions(+), 16 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 040693c00..5e46e2193 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -170,8 +170,8 @@ - in file `normedtype.v`, + new definition `type`. + new lemmas `normal_completely_regular`, `completely_reg_opc`, - `opc_weak_topology2`, `nbhs_opc_weakE`, - `locally_compact_completely_regular`, and `completely_regular_regular`. + `nbhs_opc_weakE`, `locally_compact_completely_regular`, and + `completely_regular_regular`. - in file `topology.v`, + new definitions `one_point_compactification`, and `one_point_nbhs`. + new lemmas `compact_normal_local`, `compact_normal`, `opc_compact`, diff --git a/theories/normedtype.v b/theories/normedtype.v index a2611a261..eb82287d4 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3912,22 +3912,9 @@ Qed. HB.instance Definition _ := Uniform.copy opc (completely_regular_uniformity.type completely_reg_opc). -(* TODO : fix the original*) -Lemma opc_weak_topology2 : - @nbhs _ (@weak_topology X opc Some) = @nbhs _ X. -Proof. -rewrite funeq2E => x U; apply/propeqP; split; rewrite /(@nbhs _ (weak_topology _)) /=. - case => V [[/= W] oW <- /= Ws] /filterS; apply; apply: opc_some_continuous. - exact: oW. -rewrite nbhsE; case => V [? ? ?]; exists V; split => //. -exists (Some @` V); first exact: opc_open_some. -rewrite eqEsubset; split => z /=; first by case=> ? /[swap] /Some_inj ->. -by move=> ?; exists z. -Qed. - Let X' := @weak_topology X opc Some. Lemma nbhs_opc_weakE : @nbhs X X = nbhs_ (@entourage X'). -Proof. by rewrite nbhs_entourageE opc_weak_topology2. Qed. +Proof. by rewrite nbhs_entourageE opc_weak_topology. Qed. #[local, non_forgetful_inheritance] HB.instance Definition _ := @Nbhs_isUniform.Build