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

comparison src/filter.agda @ 574:9084a26445a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZC data won't work
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jun 2022 12:49:48 +0900
parents 286016848403
children 55ab5de1ae02
comparison
equal deleted inserted replaced
573:9ec37757a5a5 574:9084a26445a7
228 F∋-p = incl U⊆F U∋-p 228 F∋-p = incl U⊆F U∋-p
229 f0 : filter F ∋ od∅ 229 f0 : filter F ∋ od∅
230 f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) ) 230 f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP {!!} {!!}) )
231 231
232 _⊆'_ : ( A B : HOD ) → Set n 232 _⊆'_ : ( A B : HOD ) → Set n
233 _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x 233 _⊆'_ A B = {x : Ordinal } → odef A x → odef B x
234 234
235 import zorn 235 import zorn
236 open zorn O _⊆'_ 236 open zorn O _⊆'_ hiding ( _⊆'_ )
237
238 open import Relation.Binary.Structures
237 239
238 MaximumSubset : {L P : HOD} 240 MaximumSubset : {L P : HOD}
239 → o∅ o< & L → o∅ o< & P → P ⊆ L 241 → o∅ o< & L → o∅ o< & P → P ⊆' L
240 → IsPartialOrderSet P 242 → (PO : IsStrictPartialOrder _≡_ _⊆'_ )
241 → ( (B : HOD) → B ⊆ P → IsTotalOrderSet B → SUP P B ) 243 → ( (B : HOD) → B ⊆ P → IsTotalOrderSet PO B → SUP PO P B )
242 → Maximal P 244 → Maximal PO P
243 MaximumSubset {L} {P} 0<L 0<P P⊆L PO SP = Zorn-lemma 0<P PO SP 245 MaximumSubset {L} {P} 0<L 0<P P⊆L PO C = Zorn-lemma PO 0<P {!!}
244 246
245 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) 247 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
246 → (F : Filter LP) → o∅ o< & L → o∅ o< & (filter F) → (¬ (filter F ∋ od∅)) → MaximumFilter LP 248 → (F : Filter LP) → o∅ o< & L → o∅ o< & (filter F) → (¬ (filter F ∋ od∅)) → MaximumFilter LP
247 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} } where 249 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} } where
248 mf01 : Maximal P 250 mf01 : Maximal {!!} {!!}
249 mf01 = MaximumSubset 0<L {!!} {!!} {!!} {!!} 251 mf01 = MaximumSubset 0<L {!!} {!!} {!!} {!!}
250 252
251 253