Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/generic-filter.agda @ 451:31f0a5a745a5
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 14 Mar 2022 19:53:54 +0900 |
| parents | b27d92694ed5 |
| children | 76aba34438f2 |
line wrap: on
line diff
--- a/src/generic-filter.agda Mon Mar 14 17:51:16 2022 +0900 +++ b/src/generic-filter.agda Mon Mar 14 19:53:54 2022 +0900 @@ -222,13 +222,19 @@ p⊆P : p ⊆ P p⊆P = ODC.power→⊆ O _ _ PP∋p df : {x : HOD} → x ⊆ P → HOD - df {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x - ... | case1 q = Incompatible.q (I p p⊆P) - ... | case2 r = Incompatible.r (I p p⊆P) + df {x} PP∋x with Incompatible.incompatible (I x PP∋x) x PP∋x + ... | case1 q = Incompatible.q (I x PP∋x) + ... | case2 r = Incompatible.r (I x PP∋x) + df¬⊆ : {x : HOD} → (lt : x ⊆ P) → ¬ ( df lt ⊆ x ) + df¬⊆ {x} PP∋x with Incompatible.incompatible (I p p⊆P) x PP∋x + ... | case1 q = {!!} + ... | case2 r = {!!} df-d : {x : HOD} → (lt : x ⊆ P) → D ∋ df lt - df-d = {!!} + df-d {x} lt = {!!} df-p : {x : HOD} → (lt : x ⊆ P) → x ⊆ df lt - df-p = {!!} + df-p {x} lt with Incompatible.incompatible (I x lt) x lt + ... | case1 q = Incompatible.p⊆q (I x lt) + ... | case2 r = Incompatible.p⊆r (I x lt) D-Dense : Dense P D-Dense = record { dense = D @@ -238,7 +244,7 @@ ; dense-p = df-p } D∩G=∅ : ( D ∩ G ) =h= od∅ - D∩G=∅ = {!!} + D∩G=∅ = ≡od∅→=od∅ ([a-b]∩b=0 {Power P} {G}) D∩G≠∅ : ¬ (( D ∩ G ) =h= od∅ ) D∩G≠∅ eq = generic (P-GenericFilter P p PP∋p C) D-Dense ( ==→o≡ eq )