X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d6043fba2c1d413fc22626fd567e18dbc34c5779;hb=67303bc29318bd94a31903a92a2127697c5de84e;hp=dcc7e9a81a86a15834228419c50ffdf9bf2b837b;hpb=06bf8cbce7fd66562954c002d4058fb18fa366cb;p=helm.git diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index dcc7e9a81..d6043fba2 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -153,7 +153,7 @@ is a peculiarity of Matita (for example in CIC as implemented by Coq they are th same). The additional restriction of not allowing the elimination of a CProp toward a Type makes the theory of Matita minimal in the following sense: - + Theorems proved in CIC as implemented in Matita can be reused in a classical and impredicative framework (i.e. forcing Matita to collapse the hierarchy of @@ -240,7 +240,7 @@ reaching the end of the formalization, but we had to assume the proof of the extensionality of the `U_x` construction (while there is no need to assume the same property for `F_x`!). -The current version of the formaliztion uses `Id`. +The current version of the formalization uses `Id`. The standard library and the `include` command ---------------------------------------------- @@ -923,11 +923,11 @@ Thus the statement `Im[d(a,i)] ⊆ V` unfolds to That, up to rewriting with the equation defining `x`, is what we mean. Since we decided to use `Id` the rewriting always work (the elimination -prnciple for `Id` is Leibnitz's equality, that is quantified over +principle for `Id` is Leibnitz's equality, that is quantified over the context. The problem that arises if we decide to make `S` a setoid is that -`V` has to be extensional w.r.t. the equality of `S` (i.e. the charactestic +`V` has to be extensional w.r.t. the equality of `S` (i.e. the characteristic functional proposition has to quotient its input with a relation bigger than the one of `S`. @@ -1013,7 +1013,7 @@ there is still some work to do. D[retr-3] To use the equation defining `b` we have to eliminate `H`. Unfolding definitions in `x` tell us there is still something to do. The `nrewrite` -tactic is a shorcut for the elimination principle of the equlity. +tactic is a shortcut for the elimination principle of the equality. It accepts an additional argument `<` or `>` to rewrite left-to-right or right-to-left. @@ -1168,15 +1168,7 @@ We now proceed with the proof of the infinity rule. D*) - -alias symbol "exists" (instance 1) = "exists". -alias symbol "covers" = "new covers set". -alias symbol "covers" = "new covers". -alias symbol "covers" = "new covers set". -alias symbol "covers" = "new covers". -alias symbol "covers" = "new covers set". -alias symbol "covers" = "new covers". -alias symbol "covers" = "new covers set". +alias symbol "covers" (instance 3) = "new covers set". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. #A; #U; #a; (** screenshot "n-cov-inf-1". *)