X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d6043fba2c1d413fc22626fd567e18dbc34c5779;hb=bf7be462a06e739b39af20f72362857e849a2aa0;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". *)