Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/Topology.agda @ 1109:f46a16cebbab
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 31 Dec 2022 17:56:01 +0900 |
parents | 720aff4a7fa4 |
children | 7fb6950b50f1 |
line wrap: on
line diff
--- a/src/Topology.agda Sat Dec 31 11:18:04 2022 +0900 +++ b/src/Topology.agda Sat Dec 31 17:56:01 2022 +0900 @@ -141,7 +141,7 @@ OS = POS TP TQ ; OS⊆PL = tp10 ; o∪ = tp13 - ; o∩ = ? + ; o∩ = tp14 } where -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y ) -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U ) @@ -162,7 +162,15 @@ tp10 : POS TP TQ ⊆ Power (ZFP P Q) tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U - tp13 {U} U⊆O = record { b = ? ; pb = ? ; bx = ? } + tp13 {U} U⊆O = tp20 U U⊆O where + ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x + ind {x} prev x⊆O = record { b = ? ; pb = ? ; bx = ? } + tp20 : (U : HOD ) → U ⊆ POS TP TQ → POS TP TQ ∋ Union U + tp20 U U⊆O = ε-induction0 { λ U → U ⊆ POS TP TQ → POS TP TQ ∋ Union U } ind U U⊆O + tp14 : {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q) + tp14 {p} {q} op oq = record { b = & tp15 ; pb = ? ; bx = ? } where + tp15 : HOD + tp15 = ? -- existence of Ultra Filter @@ -216,8 +224,3 @@ LQQ : LQ ⊆ Power Q LQQ = ? - - - - -