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

comparison src/Topology.agda @ 1154:0612874b815c

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, 18 Jan 2023 20:53:01 +0900
parents 5eb972738f9b
children c4fd0bfdfbae
comparison
equal deleted inserted replaced
1153:5eb972738f9b 1154:0612874b815c
52 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) 52 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy )
53 CS∋L : CS ∋ L 53 CS∋L : CS ∋ L
54 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where 54 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where
55 lem0 : L ＼ * (& L) ≡ od∅ 55 lem0 : L ＼ * (& L) ≡ od∅
56 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0 56 lem0 = subst (λ k → L ＼ k ≡ od∅) (sym *iso) L＼L=0
57 CS⊆PL : CS ⊆ Power L
58 CS⊆PL {x} Cx y xy = proj1 Cx xy
57 --- we may add 59 --- we may add
58 -- OS∋L : OS ∋ L 60 -- OS∋L : OS ∋ L
59 61
60 open Topology 62 open Topology
61 63
412 P∋limit : odef P limit 414 P∋limit : odef P limit
413 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F 415 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
414 416
415 -- FIP is UFL 417 -- FIP is UFL
416 418
417 record NFIP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (X : Ordinal) : Set n where 419 record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where
418 field 420 field
419 osx : * X ⊆ OS TP 421 b x : Ordinal
420 fip : {u x : Ordinal} → * u ⊆ (L ＼ * X) → Subbase (* u) x → o∅ o< x 422 0<x : o∅ o< x
421 423 b⊆X : * b ⊆ * X
422 UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) → 424 u⊆X : * u ⊆ * X
423 ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP 425 x⊆u : * x ⊆ * u
424 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where 426 sb : Subbase (* b) x
427
428 UFLP→FIP : {P : HOD} (TP : Topology P) →
429 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP
430 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
425 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 431 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
426 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x 432 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
427 N : HOD 433 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
428 N = record { od = record { def = λ X → NFIP TP LP X } ; odmax = ? ; <odmax = ? } 434 N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = ? ; <odmax = ? }
429 F : Filter {L} {P} LP 435 N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X
430 F = record { filter = N ; f⊆L = ? ; filter1 = f1 ; filter2 = ? } where 436 N⊆PX {X} CSX fp {z} nz = ?
431 f1 : {p q : HOD} → L ∋ q → N ∋ p → p ⊆ q → N ∋ q 437 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (λ lt → CS⊆PL TP (CSX lt))
432 f1 {p} {q} Lq record { osx = osx ; fip = fip } p⊆q = record { osx = ? ; fip = ? } 438 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = ? ; filter2 = ? } where
439 f1 : {p q : HOD} → * X ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
440 f1 {p} {q} Lq Np p⊆q = ?
433 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal 441 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
434 uf00 {X} CSX fip = ? 442 uf00 {X} CSX fip = ?
435 -- UFLP.limit ( uflp 443 -- UFLP.limit ( uflp
436 -- ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? )) 444 -- ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? ))
437 -- ? 445 -- ?
443 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF 451 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF
444 452
445 -- product topology of compact topology is compact 453 -- product topology of compact topology is compact
446 454
447 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) 455 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ)
448 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) LPQ uflp ) where 456 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflp ) where
449 L = pbase TP TQ 457 L = pbase TP TQ
450 LPQ = pbase⊆PL TP TQ 458 LPQ = pbase⊆PL TP TQ
451 -- Product of UFL has limit point 459 -- Product of UFL has limit point
452 uflp : (F : Filter {pbase TP TQ} LPQ) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F) 460 uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F)
453 → UFLP (ProductTopology TP TQ) LPQ F LF UF 461 → UFLP (ProductTopology TP TQ) LP F LF UF
454 uflp F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} } 462 uflp {L} LP F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} }
463
464
465