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

changeset 1177:66355bace86f

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, 22 Feb 2023 12:01:09 +0900
parents ae586d6275c2
children 7bd348551d37
files src/Topology.agda
diffstat 1 files changed, 9 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Wed Feb 22 10:11:00 2023 +0900
+++ b/src/Topology.agda	Wed Feb 22 12:01:09 2023 +0900
@@ -277,6 +277,15 @@
           →  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)
 
+fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top
+     →   ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
+fipx {L} top {X} X⊆CS fip with fip (λ x → x) (gi ?)
+... | t = ?
+
+fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top )
+     →   (fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  odef (* X) (fipx top X⊆CS fip)
+fipX∋x = ?
+
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where