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

changeset 128:69a845b82854

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... dead end?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jul 2019 19:13:43 +0900
parents 870fe02c7a07
children 2a5519dcc167
files HOD.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Mon Jul 01 16:03:15 2019 +0900
+++ b/HOD.agda	Mon Jul 01 19:13:43 2019 +0900
@@ -343,7 +343,7 @@
          --
          --  if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
-         --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
+         --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
          --
          POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t)
          POrd {A} {t} P∋t = o<→c< P∋t
@@ -359,7 +359,7 @@
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
-              lemma1 lt = ?
+              lemma1 lt = {!!}
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t