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

changeset 1139:4517d0721b59

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 Fri, 13 Jan 2023 13:16:49 +0900
parents dd18bb8d2893
children 7515d1b0570b
files src/filter.agda
diffstat 1 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Fri Jan 13 13:03:45 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 13:16:49 2023 +0900
@@ -333,6 +333,10 @@
       FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 
         ; proper = subst₂ (λ j k →  ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop  }  
           , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
+      -- 
+      -- if filter B (which contains F) is transitive, Union B is also a filter which contains F
+      --   and this is a SUP
+      -- 
       SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B
       SUP⊆ B B⊆FX OB with trio< (& B) o∅ 
       ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a )
@@ -357,8 +361,11 @@
           ... | tri< bp⊂bq ¬b ¬c = ?
           ... | tri≈ ¬a bq=bp ¬c = ?
           ... | tri> ¬a ¬b bq⊂bp = ?
+          mf32 : ¬ odef (Union B) o∅
+          mf32 record { owner = owner ; ao = bo ; ox = o0 } with proj1 ( B⊆FX bo ) 
+          ... | record { f⊆L = f⊆L ; filter1 = filter1 ; filter2 = filter2 ; proper = proper } = ⊥-elim ( proper o0 )
           mf14 : IsFilter LP (& (Union B)) 
-          mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = ? } 
+          mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = subst (λ k → ¬ odef k o∅) (sym *iso) mf32 } 
           mf15 :  filter F ⊆ Union B
           mf15 {x} Fx = record { owner = & mf20 ; ao = mf18 ; ox = subst (λ k → odef k x) (sym *iso) (mf22 Fx) } where
                mf22 : odef (filter F) x → odef mf20 x