Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1187:d996fe8dd116
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Feb 2023 01:19:24 +0900 |
| parents | ffe5bc98f9d1 |
| children | 8cbc3918d875 |
| files | src/Topology.agda src/Tychonoff.agda |
| diffstat | 2 files changed, 34 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Sat Feb 25 23:39:34 2023 +0900 +++ b/src/Topology.agda Sun Feb 26 01:19:24 2023 +0900 @@ -267,12 +267,12 @@ record FIP {L : HOD} (top : Topology L) : Set n where field limit : {X : Ordinal } → * X ⊆ CS top - → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal + → ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → Ordinal is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) + → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) + → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → {x : Ordinal } → odef (* X) x → odef L (limit CX fip) 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) @@ -338,13 +338,13 @@ fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ ) fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where -- CX is finite intersection - fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x - fip02 {C} {x} C<CX sc with trio< x o∅ + fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x + fip02 {x} sc with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri> ¬a ¬b c = c - ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* C) k) b sc } )) where - fip10 : * C ⊆ Replace' (* X) (λ z xz → L ＼ z) - fip10 {w} cw = subst (λ k → odef k w) *iso ( C<CX cw ) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* (CX ox)) k) b sc } )) where + fip10 : * (CX ox) ⊆ Replace' (* X) (λ z xz → L ＼ z) + fip10 {w} cw = subst (λ k → odef k w) *iso cw -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) fip26 : odef (* (CX ox)) (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) @@ -465,7 +465,7 @@ -- if all finite intersection of X contains something, -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) -- it means there is a limit - has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) + has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where fp07 : HOD -- we have an element of X @@ -473,15 +473,27 @@ fp08 : odef (* X) (& fp07) fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) no-cover : ¬ ( (* (OX CX)) covers L ) - no-cover cov = ⊥-elim ( o<¬≡ ? (fip (λ x → x) (fp02 (Compact.isFinite compact (OOX CX) cov))) ) where + no-cover cov = ⊥-elim ( ? ) where fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov - int : HOD - int = Replace (* fp01) (λ x → L ＼ x) - fp02 : Finite-∪ (* (OX CX)) fp01 → Subbase (* X) (& (Intersection (Replace (* fp01) (λ x → L ＼ x)))) - fp02 = ? - fp03 : * (& (Replace (* fp01) (λ x → L ＼ x))) ⊆ * X - fp03 = ? + fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) ) + fp02 t (fin-e t⊆OX ) = gi fp03 where + fp03 : odef (* X) (& (L ＼ * t)) + fp03 = ? + fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x) (fp02 ty y ) ) where + fp04 : & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) + fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where + fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x + fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt + ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where + fp06 : ¬ odef (* tx ∪ * ty) x + fp06 (case1 tx) = ¬tx tx + fp06 (case2 ty) = ¬ty ty + fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x + fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt + ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) + ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ + record NC : Set n where -- x is not covered field x : Ordinal @@ -494,7 +506,7 @@ coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) } fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ ) - fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; Lx = Lx ; yx = fp19 } ) where + fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x fp19 {y} Xy with ∨L＼X {L} {* y} {x} Lx ... | case1 yx = yx @@ -521,14 +533,14 @@ & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ & fp07 <⟨ c<→o< fp08 ⟩ & (* X) ∎ where open o≤-Reasoning O - limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) + limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal limit {X} CX fip with trio< X o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = o∅ ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c)) fip00 : {X : Ordinal} (CX : * X ⊆ CS top) - (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) + (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) fip00 {X} CX fip {x} Xx with trio< X o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
--- a/src/Tychonoff.agda Sat Feb 25 23:39:34 2023 +0900 +++ b/src/Tychonoff.agda Sun Feb 26 01:19:24 2023 +0900 @@ -68,7 +68,7 @@ fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) ) ... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where fip : {X : Ordinal} → * X ⊆ CS TP → Set n - fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x + fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } @@ -162,7 +162,7 @@ -- -- it is set of closed set and has FIP ( F is proper ) -- - ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x + ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x ufl01 = ? -- -- so we have a limit @@ -245,7 +245,7 @@ b∋z : odef nei1 z b∋z = ? bp : BaseP {P} TP Q z - bp = record { b = ? ; op = ? ; prod = ? } + bp = record { p = ? ; op = ? ; prod = ? } neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F neip = ? il2 : * z ⊆ ZFP (Power P) (Power Q)