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

changeset 1157:d6a8738ac505

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 Thu, 19 Jan 2023 17:22:02 +0900
parents c4fd0bfdfbae
children 6216562a2bce
files src/filter.agda
diffstat 1 files changed, 9 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Thu Jan 19 11:13:40 2023 +0900
+++ b/src/filter.agda	Thu Jan 19 17:22:02 2023 +0900
@@ -55,7 +55,7 @@
 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter F ∋ od∅)
-       prime   : {p q : HOD } → L ∋ p → L ∋ q  → L ∋ (p ∪ q) →  filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
+       prime   : {p q : HOD } → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
 
 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where
    field
@@ -102,12 +102,12 @@
      → ({p : HOD} → L ∋ p → L ∋ (P ＼ p))
      → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ))
      → (F : Filter {L} {P} LP) → ultra-filter F  → prime-filter F 
-filter-lemma1 {P} {L} LP NG IN F u = record {
+filter-lemma1 {P} {L} LNEG NEG CAP F u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
     } where
-  lemma3 : {p q : HOD} → L ∋ p → L ∋ q  → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
-  lemma3 {p} {q} Lp Lq _ lt with ultra-filter.ultra u Lp (NG Lp)
+  lemma3 : {p q : HOD} → L ∋ p → L ∋ q  → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q )
+  lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp (NEG Lp)
   ... | case1 p∈P  = case1 p∈P 
   ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h=  (q ∩ (P ＼ p))
@@ -119,7 +119,7 @@
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
     lemma9 : L ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (IN Lq (NG Lp))
+    lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (CAP Lq (NEG Lp))
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
     lemma6 = filter2 F lt ¬p∈P  lemma9
     lemma7 : filter F ∋ (q ∩ (P ＼ p))
@@ -135,9 +135,9 @@
 filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P)
        → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))
        → (F : Filter {L} {P} LP)  → filter F ∋ P → prime-filter F → ultra-filter F
-filter-lemma2 {P} {L} LP Lm F f∋P prime = record {
+filter-lemma2 {P} {L} LP NEG F f∋P prime = record {
          proper = prime-filter.proper prime
-       ; ultra = λ {p}  L∋p _ → prime-filter.prime prime L∋p (Lm  L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L  L∋p ))  
+       ; ultra = λ {p}  L∋p _ → prime-filter.prime prime L∋p (NEG  L∋p) (lemma p (p⊆L  L∋p ))  
    } where
         open _==_
         p⊆L : {p : HOD} → L ∋ p  → p ⊆ P
@@ -150,8 +150,6 @@
         eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p  ) = proj1 ¬p
         lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
         lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
-        lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P ＼ p))
-        lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt
 
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (suc n) where
    field
@@ -267,7 +265,7 @@
        → L ∋ p → L ∋ ( P ＼ p)) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
        → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP U
-ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
+ultra→max {L} {P} LP NEG CAP U u  = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
   is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → filter U ⊆ filter F  → (U⊂F : filter U  ⊂ filter F ) → ⊥
   is-maximum F Prop F⊆U ⟪ U<F , U⊆F ⟫   = Prop f0 where
      GT : HOD
@@ -289,7 +287,7 @@
      um00 : ¬ odef (filter U) (& p)
      um00 = proj2 (ODC.x∋minimal O GT GT≠∅)
      L∋-p : L ∋  ( P ＼ p )
-     L∋-p = NG L∋p
+     L∋-p = NEG L∋p
      U∋-p : filter U ∋  ( P ＼ p )
      U∋-p with ultra-filter.ultra u {p} L∋p L∋-p
      ... | case1 ux = ⊥-elim ( ¬U∋p ux )