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

comparison src/Tychonoff.agda @ 1224:e1a1161df14c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Tue, 07 Mar 2023 15:43:30 +0900
parents 4b6c3ed64dd1
children 5c4a088ae95b
comparison
equal deleted inserted replaced
1223:4b6c3ed64dd1 1224:e1a1161df14c
323 → UFLP TP F UF 323 → UFLP TP F UF
324 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF 324 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
325 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) 325 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F)
326 → UFLP TQ F UF 326 → UFLP TQ F UF
327 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF 327 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF
328 FPQ→FQP : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power (ZFP Q P)} {ZFP Q P } (λ x → x)
329 FPQ→FQP F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
330 projFP : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F)
331 → Filter {Power P} {P} (λ x → x)
332 projFP = ?
328 -- Product of UFL has a limit point 333 -- Product of UFL has a limit point
329 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) 334 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F)
330 → UFLP (ProductTopology TP TQ) F UF 335 → UFLP (ProductTopology TP TQ) F UF
331 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where 336 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where
332 F∋PQ : odef (filter F) (& (ZFP P Q)) 337 F∋PQ : odef (filter F) (& (ZFP P Q))
471 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq) 476 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
472 ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q ) 477 ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
473 ty51 = filter2 F ty53 ty52 ty54 478 ty51 = filter2 F ty53 ty52 ty54
474 ty50 : filter F ∋ ZFP (p ∩ q) Q 479 ty50 : filter F ∋ ZFP (p ∩ q) Q
475 ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 480 ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
476 ZFP\Q : {P Q p : HOD} → ( ZFP P Q ＼ ZFP p Q ) ≡ ZFP (P ＼ p) Q
477 ZFP\Q {P} {Q} {p} = ==→o≡ record { eq→ = ty70 ; eq← = ty71 } where
478 ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x → odef (ZFP (P ＼ p) Q) x
479 ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where
480 ty72 : odef (P ＼ p ) a
481 ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫
482 ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x
483 ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb
484 , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫
485 UFP : ultra-filter FP 481 UFP : ultra-filter FP
486 UFP = record { proper = ty61 ; ultra = ty60 } where 482 UFP = record { proper = ty61 ; ultra = ty60 } where
487 ty61 : ¬ (FPSet ∋ od∅) 483 ty61 : ¬ (FPSet ∋ od∅)
488 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where 484 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where
489 ty63 : {x : Ordinal} → ¬ odef (* z) x 485 ty63 : {x : Ordinal} → ¬ odef (* z) x
493 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az 489 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az
494 ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p)) 490 ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p))
495 ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} 491 ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q}
496 (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ? 492 (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ?
497 ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp ) 493 ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp )
498 ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) ZFP\Q) fnp )) 494 ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp ))
499 uflp : UFLP TP FP UFP 495 uflp : UFLP TP FP UFP
500 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP 496 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
501 497
502 FQ : Filter {Power Q} {Q} (λ x → x) 498 FQ : Filter {Power Q} {Q} (λ x → x)
503 FQ = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = {!!} } 499 FQ = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = {!!} }