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

diff src/filter.agda @ 1255:afecaee48825

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 Thu, 16 Mar 2023 17:46:36 +0900
parents 5223f0b40d91
children 0b7e4eb68afc
line wrap: on
line diff
--- a/src/filter.agda	Thu Mar 16 11:56:17 2023 +0900
+++ b/src/filter.agda	Thu Mar 16 17:46:36 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  → ideal ∋ (p ∪ q)
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → L ∋ (p ∩ q) → ideal ∋ (p ∪ q)
 
 open Ideal