Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 226:176ff97547b4
set theortic function definition using sup
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 11 Aug 2019 13:05:17 +0900 |
parents | 2e1f19c949dc |
children | 49736efc822b |
line wrap: on
line diff
--- a/OD.agda Sun Aug 11 08:10:13 2019 +0900 +++ b/OD.agda Sun Aug 11 13:05:17 2019 +0900 @@ -477,3 +477,9 @@ choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A choice X {A} X∋A not = x∋minimul A not +_,_ = ZF._,_ OD→ZF +Union = ZF.Union OD→ZF +Power = ZF.Power OD→ZF +Select = ZF.Select OD→ZF +Replace = ZF.Replace OD→ZF +isZF = ZF.isZF OD→ZF