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

comparison Ordinals.agda @ 258:63df67b6281c

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 Wed, 04 Sep 2019 01:12:18 +0900
parents 846e0926bb89
children 304c271b3d47
comparison
equal deleted inserted replaced
257:53b7acd63481 258:63df67b6281c
191 ; reflexive = case1 191 ; reflexive = case1
192 ; trans = OrdTrans 192 ; trans = OrdTrans
193 } 193 }
194 } 194 }
195 195
196 TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m ) 196 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
197 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) 197 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
198 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 198 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
199 → ¬ p 199 → ¬ p
200 TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 200 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
201 201