big mess of notation

[helm.git] / helm / software / matita / library / formal_topology / basic_pairs_to_basic_topologies.ma

diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
index fe4cbd10f246e339c5191a9e3125000c0c039721..fb8891613e75bbcf541e94e0fbd59b36dca5822a 100644 (file)
--- a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
@@ -52,11 +52,13 @@ record functor1 (C1: category1) (C2: category1) : Type2 ≝
 
 (*
 definition BTop_of_BP: functor1 BP BTop.
- lapply OR as F;
  constructor 1;
   [ apply basic_topology_of_basic_pair
   | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
   | simplify; intro;
   ]
 qed.
+
+lemma BBBB_faithful : failthful2 ?? VVV
+FIXME
 *)
\ No newline at end of file