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

annotate filter.agda @ 294:4340ffcfa83d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ultra-filter P → prime-filter P done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jun 2020 19:11:38 +0900
parents 9972bd4a0d6f
children 822b50091a26
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Relation.Binary.PropositionalEquality
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
16 import BAlgbra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
18 open BAlgbra O
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
19
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
20 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open OD.OD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
23 open ODAxiom odAxiom
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
25 import ODC
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
26
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
27 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
28 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
29 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
30
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
31 -- Kunen p.76 and p.53
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
32 record Filter ( L : OD ) : Set (suc n) where
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
33 field
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
34 filter : OD
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
35 f⊆PL : filter ⊆ Power L
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
36 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
37 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
38
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
39 open Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
40
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
41 -- should use inhabit?
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
42 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
43 proper-filter {L} P {p} = ¬ (filter P ∋ od∅)
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
44
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
45 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
46 prime-filter {L} P {p} {q} = filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
47
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
48 open _⊆_
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
49
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
50 trans-⊆ : { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
51 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
52
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
53 power→⊆ : ( A t : OD) → Power A ∋ t → t ⊆ A
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
54 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
55 t1 : {x : OD } → t ∋ x → ¬ ¬ (A ∋ x)
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
56 t1 = zf.IsZF.power→ isZF A t PA∋t
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
57
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
58 ∈-filter : {L p : OD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
59 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
60
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
61 ∪-lemma1 : {L p q : OD } → (p ∪ q) ⊆ L → p ⊆ L
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
62 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
63
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
64 ∪-lemma2 : {L p q : OD } → (p ∪ q) ⊆ L → q ⊆ L
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
65 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
66
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
67 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
68 q∩q⊆q = record { incl = λ lt → proj1 lt }
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
69
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
70 -- is-∅ : ( x : OD ) → Dec ( x ≡ od∅ )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
71 -- is-∅ x with is-o∅ (od→ord x)
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
72 -- ... | yes eq = yes {!!}
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
73 -- ... | no ne = no {!!}
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
74
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
75 record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
76 field
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
77 proper : ¬ (filter P ∋ od∅)
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
78 ultra : {p : OD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
79
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
80 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ultra-filter P → prime-filter {L} P {p} {q}
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
81 filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
82 ... | case1 p∈P = case1 p∈P
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
83 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
84 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) == (q ∩ (L ＼ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
85 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
86 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
87 } where
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
88 lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L ＼ p)) x → def q x
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
89 lemma4 x lt with proj1 lt
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
90 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
91 lemma4 x lt | case2 qx = qx
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
92 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
93 lemma6 = filter2 P lt ¬p∈P
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
94 lemma7 : filter P ∋ (q ∩ (L ＼ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
95 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
96 lemma8 : (q ∩ (L ＼ p)) ⊆ q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
97 lemma8 = q∩q⊆q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
98
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
99 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter P
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
100 filter-lemma2 {L} P prime p = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
101
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
102 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
103 generated-filter {L} P p = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
104
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
105 record Dense (P : OD ) : Set (suc n) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
106 field
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
107 dense : OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
108 incl : dense ⊆ P
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
109 dense-f : OD → OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
110 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p)
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
111
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
112 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
113
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
114 infinite = ZF.infinite OD→ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
115
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
116 module in-countable-ordinal {n : Level} where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
117
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
118 import ordinal
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
119
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
120 -- open ordinal.C-Ordinal-with-choice
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
121
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
122 Hω2 : Filter (Power (Power infinite))
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
123 Hω2 = {!!}
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
124
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
125
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
126 record Ideal ( L : OD ) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
127 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
128 ideal : OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
129 i⊆PL : ideal ⊆ Power L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
130 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
131 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
132
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
133 open Ideal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
134
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
135 proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
136 proper-ideal {L} P {p} = ideal P ∋ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
137
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
138 prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
139 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
140