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

diff src/filter.agda @ 1256:0b7e4eb68afc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
change to Ideal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 Mar 2023 19:01:47 +0900
parents afecaee48825
children 8a8052df5254
line wrap: on
line diff
--- a/src/filter.agda	Thu Mar 16 17:46:36 2023 +0900
+++ b/src/filter.agda	Thu Mar 16 19:01:47 2023 +0900
@@ -156,7 +156,7 @@
        ideal : HOD   
        i⊆L :  ideal ⊆ L 
        ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
-       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → L ∋ (p ∩ q) → ideal ∋ (p ∪ q)
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → L ∋ (p ∪ q) → ideal ∋ (p ∪ q)
 
 open Ideal