Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
simpler ordinal2019-06-03, by Shinji KONO
-
remove ∅-base-def2019-06-03, by Shinji KONO
-
add some lemma2019-06-03, by Shinji KONO
-
infinite and replacement begin2019-06-03, by Shinji KONO
-
Power Set on going ...2019-06-02, by Shinji KONO
-
extensionality done2019-06-02, by Shinji KONO
-
Union done2019-06-02, by Shinji KONO
-
ordinal atomical successor?2019-06-01, by Shinji KONO
-
fix ordinal2019-06-01, by Shinji KONO
-
...2019-06-01, by Shinji KONO
-
add osuc ( next larger element of Ordinal )2019-06-01, by Shinji KONO
-
Union needs +1 space2019-06-01, by Shinji KONO
-
union continue2019-05-31, by Shinji KONO
-
Union2019-05-29, by Shinji KONO
-
Added tag current for changeset 92a11dc6425c2019-05-29, by Shinji KONO
-
regularity done2019-05-29, by Shinji KONO
-
¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}2019-05-29, by Shinji KONO
-
equal2019-05-29, by Shinji KONO
-
omin2019-05-29, by Shinji KONO
-
...2019-05-29, by Shinji KONO
-
fix2019-05-29, by Shinji KONO
-
dead end2019-05-29, by Shinji KONO
-
lemma = cong₂ (λ x not → minimul x not ) oiso { }62019-05-28, by Shinji KONO
-
...2019-05-28, by Shinji KONO
-
...2019-05-28, by Shinji KONO
-
almost ...2019-05-27, by Shinji KONO
-
regurality elimination case2019-05-27, by Shinji KONO
-
fix selection axiom2019-05-27, by Shinji KONO
-
...2019-05-27, by Shinji KONO
-
tri-c<2019-05-27, by Shinji KONO
-
...2019-05-27, by Shinji KONO
-
...2019-05-25, by Shinji KONO
-
fix Select2019-05-25, by Shinji KONO
-
Added tag current for changeset 264784731a672019-05-25, by Shinji KONO
-
clean up2019-05-25, by Shinji KONO
-
== and ∅72019-05-25, by Shinji KONO
-
od∅' {n} = ord→od (o∅ {n})2019-05-24, by Shinji KONO
-
od→lv : {n : Level} → OD {n} → Nat2019-05-24, by Shinji KONO
-
equalitu and internal parametorisity2019-05-24, by Shinji KONO
-
regurality2019-05-24, by Shinji KONO
-
mnimul2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
¬ ( y c< x ) → x ≡ od∅2019-05-23, by Shinji KONO
-
transitive2019-05-22, by Shinji KONO
-
ordinal fixed2019-05-22, by Shinji KONO
-
fix oridinal2019-05-22, by Shinji KONO
-
fix2019-05-21, by Shinji KONO
-
oridnal dead end2019-05-21, by Shinji KONO
-
fix ordinal2019-05-21, by Shinji KONO
-
problem on Ordinal ( OSuc ℵ )2019-05-20, by Shinji KONO
-
posturate OD is isomorphic to Ordinal2019-05-20, by Shinji KONO
-
OD continue2019-05-19, by Shinji KONO
-
OD, HOD, TC2019-05-19, by Shinji KONO
-
dom-ψ2019-05-18, by Shinji KONO
-
...2019-05-18, by Shinji KONO
-
separte level2019-05-18, by Shinji KONO
-
Sup2019-05-17, by Shinji KONO
-
..2019-05-16, by Shinji KONO