From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Apr 2010 13:42:14 +0000 (+0000)
Subject: Formal points.
X-Git-Tag: make_still_working~2923
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=e10d227670fcc1ae0101b5a1abd8a8236d4ba5ec;p=helm.git

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 d58f69a05..813dec9fb 100644
--- 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