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

comparison src/zorn.agda @ 1072:4ce084a0dce2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
supf-mono done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 14 Dec 2022 09:19:38 +0900
parents 5463f10d6843
children b3d695340773
comparison
equal deleted inserted replaced
1071:5463f10d6843 1072:4ce084a0dce2
1233 ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where 1233 ; zo≤sz = ? ; is-minsup = ? ; cfcs = ? } where
1234 mf : ≤-monotonic-f A f 1234 mf : ≤-monotonic-f A f
1235 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 1235 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1236 mf00 : * x < * (f x) 1236 mf00 : * x < * (f x)
1237 mf00 = proj1 ( mf< x ax ) 1237 mf00 = proj1 ( mf< x ax )
1238 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = ? 1238 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? ; 0<supfz = 0<sufz
1239 ; zo≤sz = ? ; is-minsup = ? ; cfcs = cfcs } where 1239 ; zo≤sz = ? ; is-minsup = is-minsup ; cfcs = cfcs } where
1240 1240
1241 mf : ≤-monotonic-f A f 1241 mf : ≤-monotonic-f A f
1242 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where 1242 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
1243 mf00 : * x < * (f x) 1243 mf00 : * x < * (f x)
1244 mf00 = proj1 ( mf< x ax ) 1244 mf00 = proj1 ( mf< x ax )
1289 su=su = sym ( zeq _ _ (osucc u<oz) (o<→≤ <-osuc) ) 1289 su=su = sym ( zeq _ _ (osucc u<oz) (o<→≤ <-osuc) )
1290 su≡u : supfz u<x ≡ u 1290 su≡u : supfz u<x ≡ u
1291 su≡u = begin 1291 su≡u = begin
1292 ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩ 1292 ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
1293 ZChain.supf (pzc oz<x) u ≡⟨ su=u ⟩ 1293 ZChain.supf (pzc oz<x) u ≡⟨ su=u ⟩
1294 u ∎ where open ≡-Reasoning
1295
1296 chain⊆pchainU1 : {z w : Ordinal } → (z<x : z o< x) → odef (UnionCF A f ay (ZChain.supf (pzc (ob<x lim z<x))) z) w → odef pchainU w
1297 chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-init fc ⟫ = ⟪ aw , ic-init fc ⟫
1298 chain⊆pchainU1 {z} {w} z<x ⟪ aw , ch-is-sup u u<oz su=u fc ⟫
1299 = ⟪ aw , ic-isup u u<x (o≤-refl0 su≡u) (subst (λ k → FClosure A f k w ) su=su fc) ⟫ where
1300 u<x : u o< x
1301 u<x = ordtrans u<oz z<x
1302 su=su : ZChain.supf (pzc (ob<x lim z<x)) u ≡ supfz u<x
1303 su=su = sym ( zeq _ _ (o<→≤ (osucc u<oz)) (o<→≤ <-osuc) )
1304 su≡u : supfz u<x ≡ u
1305 su≡u = begin
1306 ZChain.supf (pzc (ob<x lim u<x )) u ≡⟨ sym su=su ⟩
1307 ZChain.supf (pzc (ob<x lim z<x)) u ≡⟨ su=u ⟩
1294 u ∎ where open ≡-Reasoning 1308 u ∎ where open ≡-Reasoning
1295 1309
1296 ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b } 1310 ichain-inject : {a b : Ordinal } {ia : IChain ay supfz a } {ib : IChain ay supfz b }
1297 → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib) 1311 → ZChain.supf (pzc (pic<x ia)) (IChain-i ia) o< ZChain.supf (pzc (pic<x ib)) (IChain-i ib)
1298 → IChain-i ia o< IChain-i ib 1312 → IChain-i ia o< IChain-i ib
1427 supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y 1441 supf-mono : {z y : Ordinal } → z o≤ y → supf1 z o≤ supf1 y
1428 supf-mono {z} {y} z≤y with trio< y x 1442 supf-mono {z} {y} z≤y with trio< y x
1429 ... | tri< y<x ¬b ¬c = zc01 where 1443 ... | tri< y<x ¬b ¬c = zc01 where
1430 open o≤-Reasoning O 1444 open o≤-Reasoning O
1431 zc01 : supf1 z o≤ ZChain.supf (pzc (ob<x lim y<x)) y 1445 zc01 : supf1 z o≤ ZChain.supf (pzc (ob<x lim y<x)) y
1432 zc01 with trio< z x 1446 zc01 = begin
1433 ... | tri< z<x ¬b ¬c = begin 1447 supf1 z ≡⟨ sf1=sf (ordtrans≤-< z≤y y<x) ⟩
1434 ZChain.supf (pzc (ob<x lim z<x)) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc) ⟩ 1448 ZChain.supf (pzc (ob<x lim (ordtrans≤-< z≤y y<x))) z ≡⟨ zeq _ _ (osucc z≤y) (o<→≤ <-osuc) ⟩
1435 ZChain.supf (pzc (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc (ob<x lim y<x)) z≤y ⟩ 1449 ZChain.supf (pzc (ob<x lim y<x)) z ≤⟨ ZChain.supf-mono (pzc (ob<x lim y<x)) z≤y ⟩
1436 ZChain.supf (pzc (ob<x lim y<x)) y ∎ 1450 ZChain.supf (pzc (ob<x lim y<x)) y ∎
1437 ... | tri> ¬a ¬b c = ? -- y<x x o< z → ⊥ 1451 ... | tri≈ ¬a b ¬c = zc01 where -- supf1 z o≤ spu
1438 ... | tri≈ ¬a b ¬c with osuc-≡< ( subst (λ k → k o≤ y) b z≤y) 1452 open o≤-Reasoning O
1439 ... | case1 z=y = ? -- x=z=y ⊥ 1453 zc01 : supf1 z o≤ spu
1440 ... | case2 z<y = subst₂ (λ j k → j o≤ k ) ? refl ( MinSUP.minsup ssup ? ? ) 1454 zc01 with osuc-≡< (subst (λ k → z o≤ k) b z≤y)
1441 ... | tri≈ ¬a b ¬c = ? 1455 ... | case1 z=x = o≤-refl0 (sf1=spu (sym z=x))
1442 ... | tri> ¬a ¬b c = o≤-refl0 ? 1456 ... | case2 z<x = subst (λ k → k o≤ spu ) (sym (sf1=sf z<x)) ( IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) )
1457 (MinSUP.as usup) (λ uw → MinSUP.x≤sup usup (chain⊆pchainU1 z<x uw)) )
1458 ... | tri> ¬a ¬b c = zc01 where -- supf1 z o≤ sps
1459 zc01 : supf1 z o≤ sps
1460 zc01 with trio< z x
1461 ... | tri< z<x ¬b ¬c = IsMinSUP.minsup (ZChain.is-minsup (pzc (ob<x lim z<x)) (o<→≤ <-osuc) )
1462 (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 (chain⊆pchainU1 z<x uw)) )
1463 ... | tri≈ ¬a z=x ¬c = MinSUP.minsup usup (MinSUP.as ssup) (λ uw → MinSUP.x≤sup ssup (case1 uw) )
1464 ... | tri> ¬a ¬b c = o≤-refl -- (sf1=sps c)
1443 1465
1444 0<sufz : {x : Ordinal } → o∅ o< supf1 x 1466 0<sufz : {x : Ordinal } → o∅ o< supf1 x
1445 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z)) 1467 0<sufz = ordtrans<-≤ (ZChain.0<supfz (pzc (ob<x lim 0<x ))) (OrdTrans (o≤-refl0 (sym (sf1=sf 0<x ))) (supf-mono o∅≤z))
1446 1468
1447 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z) 1469 is-minsup : {z : Ordinal} → z o≤ x → IsMinSUP A (UnionCF A f ay supf1 z) (supf1 z)