From 982eb9392e7fd9ee26a4ebf593244e8125ed7853 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Feb 2009 09:10:54 +0000 Subject: [PATCH] Hmmm, going too low. We need a more abstract proof (see Theorem 5.15, page 157 old book). --- .../formal_topology/overlap/r-o-basic_pairs.ma | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma index 92e9e975d..72c5fe02d 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma @@ -38,15 +38,23 @@ letin R ≝ (? : (carr2 (arrows2 (category2_of_category1 BP) s_1 t_1))); | constructor 1; [2: constructor 1; constructor 1; [ intros (x y); apply (y ∈ f (singleton ? x)); - | intros; unfold FunClass_1_OF_Ocontinuous_relation; + | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation; unfold in ⊢ (? ? ? (? ? ? ? ? ? %) ?); apply (.= e1‡††e); apply rule #; ] |1: constructor 1; constructor 1; [ intros (x y); apply (y ∈ star_image ?? (⊩ \sub t_1) (f (image ?? (⊩ \sub s_1) (singleton ? x)))); - | intros; unfold FunClass_1_OF_Ocontinuous_relation; + | apply hide; intros; unfold FunClass_1_OF_Ocontinuous_relation; unfold in ⊢ (? ? ? (? ? ? ? ? ? (? ? ? ? ? ? %)) ?); apply (.= e1‡(#‡†(#‡†e))); apply rule #; ] - | whd; simplify; intros; split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %; + | whd; simplify; intros; simplify; + whd in ⊢ (? % %); simplify in ⊢ (? % %); + lapply (Oreduced ?? f (image (concr s_1) (form s_1) (⊩ \sub s_1) (singleton ? x))); + [ whd in Hletin; simplify in Hletin; cases Hletin; clear Hletin; + lapply (s y); clear s; +whd in Hletin:(? ? ? (? ? (? ? ? % ?)) ?); simplify in Hletin; +whd in Hletin; simplify in Hletin; + lapply (s1 y); clear s1; + split; intros; simplify; whd in f1 ⊢ %; simplify in f1 ⊢ %; cases f1; clear f1; cases x1; clear x1; [ | exists; -- 2.39.2