From 3698de5ee6abc713534b0ee884e87e4046a087dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2009 15:04:24 +0000 Subject: [PATCH] removed useless stuff --- .../software/matita/nlibrary/topology/igft.ma | 20 ------------------- 1 file changed, 20 deletions(-) diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 8bba12281..59ccd5601 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -116,26 +116,6 @@ D*) include "sets/sets.ma". -(*HIDE*) -(* move away *) -nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W. -#A; #U; #V; #W; *; #H; #x; *; #xU; #xV; napply H; nassumption; -nqed. - -nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W. -#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption; -nqed. - -nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V. -#A; #U; #V; #W; #H1; #H2; #x; #Hx; @; ##[ napply H1; ##| napply H2; ##] nassumption; -nqed. - -ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ - sig_intro : ∀x:A.P x → sigma A P. - -interpretation "sigma" 'sigma \eta.p = (sigma ? p). -(*UNHIDE*) - (*D Some basic results that we will use are also part of the sets library: -- 2.39.2