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

changeset 1109:f46a16cebbab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Dec 2022 17:56:01 +0900
parents 720aff4a7fa4
children 7fb6950b50f1
files src/OD.agda src/Topology.agda
diffstat 2 files changed, 19 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/OD.agda	Sat Dec 31 11:18:04 2022 +0900
+++ b/src/OD.agda	Sat Dec 31 17:56:01 2022 +0900
@@ -296,6 +296,15 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
 
+ε-induction0 : { ψ : HOD  → Set n}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction0 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso )))
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
+     ε-induction-ord ox {oy} lt = inOrdinal.TransFinite0 O {λ oy → ψ (* oy)} induction oy
+
 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup
 ¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
 ¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where
--- a/src/Topology.agda	Sat Dec 31 11:18:04 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 17:56:01 2022 +0900
@@ -141,7 +141,7 @@
        OS    = POS TP TQ
     ;  OS⊆PL = tp10
     ;  o∪ = tp13
-    ;  o∩ = ?
+    ;  o∩ = tp14
   } where
         --  B : (OS P ∋ x →  proj⁻¹ x ) ∨ (OS Q ∋ y  →  proj⁻¹ y )
         --  U ⊂ ZFP P Q  ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧  b ⊂ U )
@@ -162,7 +162,15 @@
         tp10 : POS TP TQ ⊆ Power (ZFP P Q)
         tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz
         tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
-        tp13 {U} U⊆O  = record { b = ? ; pb = ? ; bx = ? } 
+        tp13 {U} U⊆O  = tp20 U U⊆O where
+             ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x
+             ind {x} prev x⊆O = record { b = ? ; pb = ? ; bx = ? }
+             tp20 : (U : HOD ) →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U 
+             tp20 U U⊆O = ε-induction0 { λ U →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U } ind U U⊆O
+        tp14 :  {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q)
+        tp14 {p} {q} op oq  = record { b = & tp15 ; pb = ? ; bx = ? } where
+             tp15 : HOD
+             tp15 = ?
 
 -- existence of Ultra Filter 
 
@@ -216,8 +224,3 @@
          LQQ : LQ ⊆ Power Q
          LQQ = ?
 
-
-
-
-
-