Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Tychonoff.agda @ 1202:d6781ad8149e
...
author | kono |
---|---|
date | Thu, 02 Mar 2023 12:42:22 +0800 |
parents | 03684784bc5f |
children | 2f09ce1dd2a1 |
comparison
equal
deleted
inserted
replaced
1201:03684784bc5f | 1202:d6781ad8149e |
---|---|
91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD | 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) | 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } | 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P | 94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb | 95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
96 -- filter base is not empty | |
96 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD | 97 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD |
97 nc {X} CSX fip with trio< o∅ X | 98 nc {X} CSX fip with trio< o∅ X |
98 ... | tri< 0<X ¬b ¬c = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where | 99 ... | tri< 0<X ¬b ¬c = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where |
99 e : HOD -- we have an element of X | 100 e : HOD -- we have an element of X |
100 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | 101 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) |