Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1101:7ce2cc622c92
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 28 Dec 2022 18:14:29 +0900 |
parents | 40345abc0949 |
children | d122d0c1b094 |
comparison
equal
deleted
inserted
replaced
1100:c90eec304cfa | 1101:7ce2cc622c92 |
---|---|
1107 | 1107 |
1108 ... | no lim with trio< x o∅ | 1108 ... | no lim with trio< x o∅ |
1109 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 1109 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1110 ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; supf-mono = λ _ → o≤-refl | 1110 ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; supf-mono = λ _ → o≤-refl |
1111 ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where | 1111 ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0))) } where |
1112 -- initial case | |
1112 | 1113 |
1113 mf : ≤-monotonic-f A f | 1114 mf : ≤-monotonic-f A f |
1114 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where | 1115 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where |
1115 mf00 : * x < * (f x) | 1116 mf00 : * x < * (f x) |
1116 mf00 = proj1 ( mf< x ax ) | 1117 mf00 = proj1 ( mf< x ax ) |