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

comparison OD.agda @ 226:176ff97547b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
225:5f48299929ac 226:176ff97547b4
475 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD 475 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
476 choice-func X {x} not X∋x = minimul x not 476 choice-func X {x} not X∋x = minimul x not
477 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 477 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
478 choice X {A} X∋A not = x∋minimul A not 478 choice X {A} X∋A not = x∋minimul A not
479 479
480 _,_ = ZF._,_ OD→ZF
481 Union = ZF.Union OD→ZF
482 Power = ZF.Power OD→ZF
483 Select = ZF.Select OD→ZF
484 Replace = ZF.Replace OD→ZF
485 isZF = ZF.isZF OD→ZF