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

changeset 834:6bf0899a6150

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 Tue, 23 Aug 2022 11:25:55 +0900
parents 3fa321cbc337
children 106492766e36
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Aug 23 10:33:47 2022 +0900
+++ b/src/zorn.agda	Tue Aug 23 11:25:55 2022 +0900
@@ -783,6 +783,17 @@
              field
                 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 
 
+          initial-segment : {a b z : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
+              →  a o≤ b 
+              →  ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z o≤  ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
+          initial-segment = ?
+
+          is01 : {a b : Ordinal } → (a<x : a o< x )   → (b<x : b o< x )   
+              →  a o≤ b 
+              UnionCF A f mf ay (ZChain.supf (pzc (osuc a) (ob<x lim a<x ))) x ⊆'
+              UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim b<x ))) x 
+          is01 = ?
+
           supf1 : Ordinal → Ordinal
           supf1 z = ?
           -- ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z