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

changeset 1271:dc5abc7b8473

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 Sun, 26 Mar 2023 20:30:46 +0900
parents 905311ffe7ec
children 2a176e2694ab
files src/generic-filter.agda
diffstat 1 files changed, 6 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sun Mar 26 17:18:45 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 26 20:30:46 2023 +0900
@@ -368,6 +368,12 @@
        G∋gi : odef (⊆-Ideal.ideal (genf G)) gi
        x∋gi : odef (* x) gi
 
+MgH : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
+MgH {L} {P} LP M G = record { od = record { def = λ x → odef M x ∧ Mg LP M G x } ; odmax = & M ; <odmax = odef∧<  }
+
+MG : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
+MG {L} {P} LP M G = M ∪ Union (MgH LP M G)
+
 TCS : (G : HOD) → Set (Level.suc n)
 TCS G = {x y : HOD} → G ∋ x → x ∋ y → G ∋ y