# HG changeset patch # User Shinji KONO # Date 1592031550 -32400 # Node ID 773e03dfd6ede9a2092799a08e02413aab1f59d7 # Parent ef93c56ad3115a1ecb36197dde0848d6a4b4cd67 ... diff -r ef93c56ad311 -r 773e03dfd6ed filter.agda --- a/filter.agda Fri Jun 12 19:21:14 2020 +0900 +++ b/filter.agda Sat Jun 13 15:59:10 2020 +0900 @@ -33,32 +33,37 @@ A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } +-- Kunen p.76 and p.53 record Filter ( L : OD ) : Set (suc n) where field filter : OD - ¬f∋∅ : ¬ ( filter ∋ od∅ ) - f∋L : filter ∋ L f⊆PL : filter ⊆ Power L filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) +open Filter + +proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n +proper-filter {L} P {p} = filter P ∋ L + +prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n +prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) + record Ideal ( L : OD ) : Set (suc n) where field ideal : OD - i∋∅ : ideal ∋ od∅ - ¬i∋L : ¬ ( ideal ∋ L ) i⊆PL : ideal ⊆ Power L ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) -open Filter open Ideal -L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L -L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!} +proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n +proper-ideal {L} P {p} = ideal P ∋ od∅ -prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n -prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) +prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n +prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) + ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )