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

comparison Ordinals.agda @ 420:53422a8ea836

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bijection
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Jul 2020 17:42:25 +0900
parents aa306f5dab9b
children 9984cdd88da3
comparison
equal deleted inserted replaced
419:4af94768e372 420:53422a8ea836
311 omax<nx {x} {y} {z} x<nz y<nz with trio< x y 311 omax<nx {x} {y} {z} x<nz y<nz with trio< x y
312 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz 312 omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
313 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz 313 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
314 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz 314 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
315 315
316 nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
317 nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
318 nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
319 nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
320 nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
321
316 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where 322 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
317 field 323 field
318 os→ : (x : Ordinal) → x o< maxordinal → Ordinal 324 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
319 os← : Ordinal → Ordinal 325 os← : Ordinal → Ordinal
320 os←limit : (x : Ordinal) → os← x o< maxordinal 326 os←limit : (x : Ordinal) → os← x o< maxordinal