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

comparison src/Topology.agda @ 1178:7bd348551d37

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji Kono
date Thu, 23 Feb 2023 09:58:11 +0800
parents 66355bace86f
children f4cd937759fc
comparison
equal deleted inserted replaced
1177:66355bace86f 1178:7bd348551d37
277 → odef L (limit CX fip) 277 → odef L (limit CX fip)
278 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) 278 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
279 279
280 fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top 280 fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top
281 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal 281 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal
282 fipx {L} top {X} X⊆CS fip with fip (λ x → x) (gi ?) 282 fipx {L} top {X} X⊆CS fip with trio< X o∅
283 ... | t = ? 283 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
284 ... | tri≈ ¬a b ¬c = o∅
285 ... | tri> ¬a ¬b c = & (ODC.minimal O (* fip00) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) ( fip (λ x → x ) (gi ? ) )))) where
286 fip00 : ?
287 fip00 = & (ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) c ) ))
284 288
285 fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top ) 289 fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top )
286 → (fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → odef (* X) (fipx top X⊆CS fip) 290 → (fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → odef (* X) (fipx top X⊆CS fip)
287 fipX∋x = ? 291 fipX∋x {L} top {X} X⊆CS fip with trio< X o∅
292 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
293 ... | tri≈ ¬a b ¬c = ?
294 ... | tri> ¬a ¬b c = ? -- fip (λ x → x) (gi ?)
288 295
289 -- Compact 296 -- Compact
290 297
291 data Finite-∪ (S : HOD) : Ordinal → Set n where 298 data Finite-∪ (S : HOD) : Ordinal → Set n where
292 fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x 299 fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
466 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top 473 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top
467 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox 474 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
468 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where 475 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where
469 comp01 : odef (* X) (& (* z)) 476 comp01 : odef (* X) (& (* z))
470 comp01 = subst (λ k → odef (* X) k) (sym &iso) az 477 comp01 = subst (λ k → odef (* X) k) (sym &iso) az
471 -- 478
472 -- if all finite intersection of (OX X) contains something, 479 -- if all finite intersection of (OX X) contains something,
473 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) 480 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
474 -- it means there is a limit 481 -- it means there is a limit
475 -- 482 --
476 Intersection : (X : Ordinal ) → o∅ o< X → HOD -- ∩ X 483 Intersection : (X : Ordinal ) → o∅ o< X → HOD -- ∩ X