Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index d58f69a05fdc1aafe5b4894eedd2ce7a05ad639e..813dec9fb1162617267a0ca1824e07db5a6b1a40 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -226,9 +226,21 @@ nlemma ftcoleqleft:
  #A; #F; #a; #H; ncases H; /2/.
 nqed.
 
+(*CSC: non serve manco questo (vedi sotto) *)
+nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
+ #A; //.
+nqed.
+
 alias symbol "I" (instance 6) = "I".
 ntheorem ftcoinfinity: ∀A: Ax_pro. ∀F: Ω^A. ∀a. a ⋉ F → (∀i: 𝐈 a. ∃b. b ∈ 𝐂 a i ∧ b ⋉ F).
  #A; #F; #a; #H; #i; nlapply (ftcoleqinfinity … F … a … i); //; #H;
  ncases H; #c; *; *; *; #b; *; #H1; #H2; #H3; #H4; @ b; @ [ napply H1 (*CSC: auto non va *)]
  napply (ftcoleqleft … c); //.
-nqed.
\ No newline at end of file
+nqed.
+
+nrecord Pt (A: Ax_pro) : Type[1] ≝
+ { pt_set: Ω^A;
+   pt_inhabited: ∃a. a ∈ pt_set;
+   pt_filtering: ∀a,b. a ∈ pt_set → b ∈ pt_set → ∃c. c ∈ (singleton … a) ↓ (singleton … b) → c ∈ pt_set;
+   pt_closed: {b | b ⋉ pt_set} ⊆ pt_set   
+ }.
\ No newline at end of file