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

comparison filter.agda @ 290:359402cc6c3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
definition of filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jun 2020 19:19:16 +0900
parents d9d3654baee1
children ef93c56ad311
comparison
equal deleted inserted replaced
286:4ae48eed654a 290:359402cc6c3d
33 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } 33 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
34 34
35 35
36 record Filter ( L : OD ) : Set (suc n) where 36 record Filter ( L : OD ) : Set (suc n) where
37 field 37 field
38 filter : OD 38 filter : OD
39 proper : ¬ ( filter ∋ od∅ ) 39 ¬f∋∅ : ¬ ( filter ∋ od∅ )
40 inL : filter ⊆ L 40 f∋L : filter ∋ L
41 f⊆PL : filter ⊆ Power L
41 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q 42 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
42 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 43 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
43 44
45 record Ideal ( L : OD ) : Set (suc n) where
46 field
47 ideal : OD
48 i∋∅ : ideal ∋ od∅
49 ¬i∋L : ¬ ( ideal ∋ L )
50 i⊆PL : ideal ⊆ Power L
51 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
52 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
53
44 open Filter 54 open Filter
55 open Ideal
45 56
46 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L 57 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
47 L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!} 58 L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!}
48 59
49 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n 60 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
50 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 61 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
51 62
52 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n 63 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n
60 filter-lemma2 {L} P prime p with prime {!!} 71 filter-lemma2 {L} P prime p with prime {!!}
61 ... | t = {!!} 72 ... | t = {!!}
62 73
63 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 74 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
64 generated-filter {L} P p = record { 75 generated-filter {L} P p = record {
65 proper = {!!} ; 76 filter = {!!} ;
66 filter = {!!} ; inL = {!!} ;
67 filter1 = {!!} ; filter2 = {!!} 77 filter1 = {!!} ; filter2 = {!!}
68 } 78 }
69 79
70 record Dense (P : OD ) : Set (suc n) where 80 record Dense (P : OD ) : Set (suc n) where
71 field 81 field