Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1246:dd3debafba2d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2023 13:17:31 +0900
parents 11049e3168ad
children 0350fe03d73a
files src/generic-filter.agda
diffstat 1 files changed, 17 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Tue Mar 14 11:58:15 2023 +0900
+++ b/src/generic-filter.agda	Tue Mar 14 13:17:31 2023 +0900
@@ -350,26 +350,37 @@
       p⊆r : p ⊆ r  
       ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
 
-lemma232 : (P L p0 : HOD ) → (LP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
+lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
       → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))  -- L is a Boolean Algebra
       → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
       → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
       → (C : CountableModel ) 
       → ( MP : ctl-M C ∋ P )
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
-      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG  C ))
-lemma232 P L p0 LP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D)) 
+      →  ¬ ( ctl-M C ∋  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C ))
+lemma232 P L p0 LPP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D)) 
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
-    gf =  rgen ( P-GenericFilter P L p0 LP Lp0 CAP UNI NEG  C )
+    gf =  rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG  C )
     M = ctl-M C
     D : HOD  
     D = L ＼ gf
     M∋D : M ∋ D
     M∋D = ?
+    D⊆PP : D ⊆ Power P
+    D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
+    DD : Dense {L} {P} LPP
+    Dense.dense DD = D
+    Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx
+    Dense.dense-f DD Lp = ? where
+        ll00 : HOD
+        ll00 with NotCompatible.¬compat (NC Lp)
+        ... | nc = ? where
+           ll01 : {q r : HOD } → (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s)) → (¬ (gf ∋ q)) ∨ (¬ (gf ∋ q))
+           ll01 = ?
+    Dense.dense-d DD = ?
+    Dense.dense-p DD = ?
     ¬gf∩D=0 : ¬ ( (gf ∩ D) =h= od∅ )
     ¬gf∩D=0 = ?
-    gf∩D∋x :  (gf ∩ D) ∋ ?
-    gf∩D∋x = ?
 
 --
 -- P-Generic Filter defines a countable model D ⊂ C from P