From e10d227670fcc1ae0101b5a1abd8a8236d4ba5ec Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Apr 2010 13:42:14 +0000 Subject: [PATCH] Formal points. From: sacerdot --- helm/software/matita/nlibrary/arithmetics/R.ma | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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 -- 2.39.2