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

comparison Ordinals.agda @ 309:d4802179a66f

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, 30 Jun 2020 00:17:05 +0900
parents b172ab9f12bc
children 21203fe0342f
comparison
equal deleted inserted replaced
308:b172ab9f12bc 309:d4802179a66f
198 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) 198 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
199 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 199 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
200 → ¬ p 200 → ¬ p
201 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 201 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
202 202
203 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
204 field
205 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
206 os← : Ordinal → Ordinal
207 os←limit : (x : Ordinal) → os← x o< maxordinal
208 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
209 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
210