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

changeset 449:be685f338fdc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generic Filter done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2022 19:22:12 +0900
parents 81691a6b352b
children b27d92694ed5
files src/generic-filter.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sun Mar 13 19:03:33 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 13 19:22:12 2022 +0900
@@ -185,10 +185,14 @@
            fd = dense-f D p0
            PP∋D : dense D ⊆ Power P
            PP∋D = d⊆P D
+           fd00 : PDHOD P p0 C ∋ p0
+           fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = Pp0 }
            fd02 : dense D ∋ dense-f D p0 
            fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
+           fd04 : dense-f D p0 ⊆ P
+           fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
            fd03 : PDHOD P p0 C  ∋ dense-f D p0 
-           fd03 = f1 {p0} {dense-f D p0} {!!} {!!} ( dense-p D {!!} )
+           fd03 = f1 {p0} {dense-f D p0} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
            fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
            fd01 = ⟪ fd02 , fd03 ⟫