From d4cd2564126b15d4f0aa736353d25dfc34d2cad8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 29 Jan 2009 11:48:31 +0000 Subject: [PATCH] ... --- .../overlap/basic_topologies_to_o-basic_topologies.ma | 2 +- .../formal_topology/overlap/saturations_to_o-saturations.ma | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma index 6b6469f27..ee9682cec 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma @@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma". definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology. intro; constructor 1; - [ apply (SUBSETS b); + [ apply (POW' b); | apply (A b); | apply (J b); | apply (A_is_saturation b); diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma index 97bfcd6c9..88a18fda7 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma @@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma". (* These are only conversions :-) *) definition o_operator_of_operator: - ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C). + ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C). intros (C t);apply t; qed. -- 2.39.2