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

changeset 263:2e75710a936b

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 Mon, 23 Sep 2019 09:16:39 +0900
parents 53744836020b
children fee0fab14de0
files ordinal.agda
diffstat 1 files changed, 7 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal.agda	Sun Sep 22 20:26:32 2019 +0900
+++ b/ordinal.agda	Mon Sep 23 09:16:39 2019 +0900
@@ -261,10 +261,10 @@
        caseOSuc lx ox prev = {!!}
 
   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
-  continuum-hyphotheis a x lt = lemma where
-       lemma : Ord (osuc a) ∋ x
-       lemma with IsZF.power→ isZF (Ord a) x lt {{!!}} {!!} 
-       ... | t = {!!}
-
-
-
+  continuum-hyphotheis a x = lemma2 where
+       lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
+       lemma1 = {!!}
+       lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
+       lemma = o<→c< lemma1
+       lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
+       lemma2 = {!!}