Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
...2022-03-01, by Shinji KONO
-
give up this generic filter definition2022-03-01, by Shinji KONO
-
...2022-02-26, by Shinji KONO
-
⊆-reduction2022-02-25, by Shinji KONO
-
val2022-02-22, by Shinji KONO
-
...2022-02-22, by Shinji KONO
-
fi;ter12022-02-20, by Shinji KONO
-
generic filter2022-02-18, by Shinji KONO
-
separate PFOD2021-09-03, by Shinji KONO
-
Added tag current for changeset a5f8084b83682020-12-21, by Shinji KONO
-
reorganiztion for apkg2020-12-21, by Shinji KONO
-
...2020-12-20, by Shinji KONO
-
...2020-12-19, by Shinji KONO
-
add Topology2020-12-19, by Shinji KONO
-
...2020-08-08, by Shinji KONO
-
...2020-08-06, by Shinji KONO
-
...2020-08-05, by Shinji KONO
-
remvoe TransFinifte12020-08-01, by Shinji KONO
-
...2020-08-01, by Shinji KONO
-
syntax *, &, ⟪ , ⟫2020-08-01, by Shinji KONO
-
...2020-07-31, by Shinji KONO
-
bijection2020-07-31, by Shinji KONO
-
...2020-07-31, by Shinji KONO
-
...2020-07-31, by Shinji KONO
-
...2020-07-31, by Shinji KONO
-
...2020-07-30, by Shinji KONO
-
...2020-07-30, by Shinji KONO
-
add VL2020-07-30, by Shinji KONO
-
generic filter on going2020-07-29, by Shinji KONO
-
...2020-07-29, by Shinji KONO
-
...2020-07-29, by Shinji KONO
-
...2020-07-29, by Shinji KONO
-
nat→ω-iso2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
...2020-07-28, by Shinji KONO
-
use induction2020-07-27, by Shinji KONO
-
...2020-07-27, by Shinji KONO
-
...2020-07-27, by Shinji KONO
-
...2020-07-27, by Shinji KONO
-
...2020-07-27, by Shinji KONO
-
...2020-07-27, by Shinji KONO
-
...2020-07-26, by Shinji KONO
-
...2020-07-26, by Shinji KONO
-
...2020-07-25, by Shinji KONO
-
generic filter defined2020-07-25, by Shinji KONO
-
generic filter2020-07-25, by Shinji KONO
-
...2020-07-25, by Shinji KONO
-
...2020-07-25, by Shinji KONO
-
...2020-07-25, by Shinji KONO
-
...2020-07-23, by Shinji KONO
-
...2020-07-21, by Shinji KONO
-
Three List / Filter2020-07-21, by Shinji KONO
-
...2020-07-21, by Shinji KONO
-
...2020-07-21, by Shinji KONO
-
...2020-07-21, by Shinji KONO
-
...2020-07-20, by Shinji KONO
-
...2020-07-20, by Shinji KONO
-
...2020-07-20, by Shinji KONO
-
..2020-07-20, by Shinji KONO
-
...2020-07-20, by Shinji KONO
-
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work2020-07-20, by Shinji KONO
-
...2020-07-20, by Shinji KONO
-
...2020-07-19, by Shinji KONO
-
...2020-07-19, by Shinji KONO
-
...2020-07-19, by Shinji KONO
-
...2020-07-19, by Shinji KONO
-
fix Select and Replace2020-07-19, by Shinji KONO
-
...2020-07-18, by Shinji KONO
-
...2020-07-18, by Shinji KONO
-
...2020-07-18, by Shinji KONO
-
...2020-07-18, by Shinji KONO
-
...2020-07-18, by Shinji KONO
-
hω22020-07-18, by Shinji KONO
-
...2020-07-17, by Shinji KONO
-
...2020-07-17, by Shinji KONO
-
...2020-07-14, by Shinji KONO
-
...2020-07-14, by Shinji KONO
-
...2020-07-14, by Shinji KONO
-
Removed tag curret2020-07-14, by Shinji KONO
-
Added tag release for changeset 45fefbfd48712020-07-14, by Shinji KONO
-
Added tag current for changeset aa03b9c289c02020-07-14, by Shinji KONO
-
Limit Ordinal2020-07-14, by Shinji KONO
-
Added tag current for changeset e277699923992020-07-14, by Shinji KONO
-
next-is-limit2020-07-14, by Shinji KONO
-
mistake2020-07-14, by Shinji KONO
-
...2020-07-14, by Shinji KONO
-
...2020-07-14, by Shinji KONO
-
Limit ordinal and possible OD bound2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
Added tag curret for changeset e0916a6329712020-07-13, by Shinji KONO
-
possible order restriction makes ω ZFSet2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
...2020-07-13, by Shinji KONO
-
...2020-07-12, by Shinji KONO
-
...2020-07-12, by Shinji KONO
-
...2020-07-07, by Shinji KONO
-
...2020-07-06, by Shinji KONO
-
...2020-07-06, by Shinji KONO
-
Added tag release for changeset fcc65e37e72b2020-07-05, by Shinji KONO
-
Added tag current for changeset 12071f79f3cf2020-07-05, by Shinji KONO
-
HOD done2020-07-05, by Shinji KONO
-
...2020-07-05, by Shinji KONO
-
...2020-07-05, by Shinji KONO
-
intoduce ωmax2020-07-05, by Shinji KONO
-
...2020-07-04, by Shinji KONO
-
...2020-07-04, by Shinji KONO
-
...2020-07-04, by Shinji KONO
-
...2020-07-04, by Shinji KONO
-
...2020-07-04, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
infinite ...2020-07-03, by Shinji KONO
-
Union done2020-07-03, by Shinji KONO
-
Replace max2020-07-03, by Shinji KONO
-
Power done2020-07-03, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
...2020-07-03, by Shinji KONO
-
...2020-07-02, by Shinji KONO
-
...2020-06-30, by Shinji KONO
-
...2020-06-29, by Shinji KONO
-
...2020-06-29, by Shinji KONO
-
...2020-06-29, by Shinji KONO
-
...2020-06-29, by Shinji KONO
-
fix sup2020-06-29, by Shinji KONO
-
...2020-06-29, by Shinji KONO
-
HOD using <maxod2020-06-29, by Shinji KONO
-
¬odmax based HOD2020-06-29, by Shinji KONO
-
HOD and reduction mapping of Ordinals2020-06-28, by Shinji KONO
-
contradiction found ...2020-06-24, by Shinji KONO
-
-- the set of finite partial functions from ω to 22020-06-23, by Shinji KONO
-
better to use ordinal number hierachy to create HOD2020-06-23, by Shinji KONO
-
... should we use HOD?2020-06-23, by Shinji KONO
-
maxod try2020-06-22, by Shinji KONO
-
if Filter contains L, prime filter is ultra2020-06-15, by Shinji KONO
-
fix prime2020-06-15, by Shinji KONO
-
ultra-filter P → prime-filter P done2020-06-14, by Shinji KONO
-
...2020-06-13, by Shinji KONO
-
...2020-06-13, by Shinji KONO
-
...2020-06-12, by Shinji KONO
-
definition of filter2020-06-12, by Shinji KONO
-
...2020-06-07, by Shinji KONO
-
Added tag current for changeset 313140ae5e3d2020-05-10, by Shinji KONO
-
clean up2020-05-10, by Shinji KONO
-
minimal from LEM2020-05-10, by Shinji KONO
-
...2020-05-09, by Shinji KONO
-
...2020-05-09, by Shinji KONO
-
...2020-05-09, by Shinji KONO
-
...2020-05-09, by Shinji KONO
-
...2020-05-09, by Shinji KONO
-
Added tag current for changeset d9d3654baee12020-05-09, by Shinji KONO
-
seperate choice from LEM2020-05-09, by Shinji KONO
-
separate choice2020-05-09, by Shinji KONO
-
Added tag current for changeset 29a85a427ed22020-04-25, by Shinji KONO
-
ε-induction2020-04-25, by Shinji KONO
-
add documents2020-01-11, by Shinji KONO
-
separate ordered pair and Boolean Algebra2019-12-31, by Shinji KONO
-
fix incl2019-12-30, by Shinji KONO
-
...2019-10-06, by Shinji KONO
-
disjunction and conjunction2019-10-06, by Shinji KONO
-
...2019-09-30, by Shinji KONO
-
⊆2019-09-30, by Shinji KONO
-
...2019-09-30, by Shinji KONO
-
filter2019-09-30, by Shinji KONO
-
...2019-09-23, by Shinji KONO
-
...2019-09-23, by Shinji KONO
-
CH trying ...2019-09-22, by Shinji KONO
-
ε-induction from TransFinite induction2019-09-17, by Shinji KONO
-
sup with limit give up2019-09-05, by Shinji KONO
-
...2019-09-04, by Shinji KONO
-
...2019-09-03, by Shinji KONO
-
move product to OD2019-08-30, by Shinji KONO
-
Added tag current for changeset 2ea2a19f9cd62019-08-29, by Shinji KONO
-
ordered pair clean up2019-08-29, by Shinji KONO
-
proudct uniquness done2019-08-29, by Shinji KONO
-
give up product uniquness2019-08-28, by Shinji KONO
-
...2019-08-28, by Shinji KONO
-
...2019-08-28, by Shinji KONO
-
...2019-08-28, by Shinji KONO
-
prod-eq done2019-08-27, by Shinji KONO
-
fix pair2019-08-26, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
new assumption2019-08-25, by Shinji KONO
-
Product2019-08-25, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
...2019-08-22, by Shinji KONO
-
fix2019-08-21, by Shinji KONO
-
...2019-08-20, by Shinji KONO
-
ZFProduct2019-08-19, by Shinji KONO
-
...2019-08-18, by Shinji KONO
-
...2019-08-16, by Shinji KONO
-
fix cardinal2019-08-14, by Shinji KONO
-
ac from LEM in abstract ordinal2019-08-13, by Shinji KONO
-
function continue2019-08-12, by Shinji KONO
-
Added tag current for changeset 1b1620e2053c2019-08-11, by Shinji KONO
-
we need ordered pair2019-08-11, by Shinji KONO
-
...2019-08-11, by Shinji KONO
-
try transfinite2019-08-11, by Shinji KONO
-
...2019-08-11, by Shinji KONO
-
set theortic function definition using sup2019-08-11, by Shinji KONO
-
does not work2019-08-10, by Shinji KONO
-
recover ε-induction2019-08-10, by Shinji KONO
-
sepration of ordinal from OD2019-08-09, by Shinji KONO
-
TransFinite induction fixed2019-08-09, by Shinji KONO
-
fix Ordinals2019-08-08, by Shinji KONO
-
try to separate Ordinals2019-08-07, by Shinji KONO
-
separate cardinal2019-08-07, by Shinji KONO
-
try func2019-08-06, by Shinji KONO
-
cardinal continue2019-08-05, by Shinji KONO
-
Cardinal start2019-08-04, by Shinji KONO
-
Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision2019-08-02, by Shinji KONO
-
both2019-08-02, by Shinji KONO
-
separate logic and nat2019-08-02, by Shinji KONO
-
Added tag current for changeset 2c7d45734e3b2019-08-01, by Shinji KONO
-
axiom of choice from exclusive middle done2019-08-01, by Shinji KONO
-
∀-imply-or2019-08-01, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
try again ..2019-07-31, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
Transfinite induction fixed2019-07-31, by Shinji KONO
-
fixing transfinte induction...2019-07-31, by Shinji KONO
-
ε-induction like loop again2019-07-30, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
ε-induction again2019-07-29, by Shinji KONO
-
curry form2019-07-29, by Shinji KONO
-
another approach2019-07-29, by Shinji KONO
-
transfinite2019-07-29, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
emulate ε-induction proof2019-07-29, by Shinji KONO
-
...2019-07-28, by Shinji KONO
-
does not work2019-07-28, by Shinji KONO
-
choice function cannot jump between ordinal level2019-07-28, by Shinji KONO
-
add filter2019-07-26, by Shinji KONO
-
Axiom of choies implies p ∨ ( ¬ p )2019-07-25, by Shinji KONO
-
axiom of choice → p ∨ ¬ p2019-07-25, by Shinji KONO
-
add Todo2019-07-23, by Shinji KONO
-
fix extensionality2019-07-22, by Shinji KONO
-
...2019-07-22, by Shinji KONO
-
...2019-07-22, by Shinji KONO
-
fix zf2019-07-21, by Shinji KONO
-
remove ordinal-definable2019-07-21, by Shinji KONO
-
...2019-07-21, by Shinji KONO
-
new ordinal-definable2019-07-20, by Shinji KONO
-
fix comments2019-07-19, by Shinji KONO
-
Added tag current for changeset ecb329ba38ac2019-07-19, by Shinji KONO
-
ε-induction done2019-07-19, by Shinji KONO
-
...2019-07-19, by Shinji KONO
-
...2019-07-19, by Shinji KONO
-
...2019-07-19, by Shinji KONO
-
non terminateing on ε-induction2019-07-19, by Shinji KONO
-
...2019-07-18, by Shinji KONO
-
...2019-07-18, by Shinji KONO
-
trans finite on ε-induction2019-07-18, by Shinji KONO
-
...2019-07-18, by Shinji KONO
-
...2019-07-18, by Shinji KONO
-
use double negation2019-07-17, by Shinji KONO
-
minor fix2019-07-16, by Shinji KONO
-
Added tag current for changeset b06f5d2f34b12019-07-15, by Shinji KONO
-
Axiom of choice2019-07-15, by Shinji KONO
-
ininite done2019-07-15, by Shinji KONO
-
...2019-07-15, by Shinji KONO
-
infinite continue...2019-07-15, by Shinji KONO
-
Union trans finite2019-07-14, by Shinji KONO
-
explict logical definition of Union failed2019-07-13, by Shinji KONO
-
differeent Union approach2019-07-11, by Shinji KONO
-
union continue2019-07-10, by Shinji KONO
-
union trying ..2019-07-10, by Shinji KONO
-
union continue ...2019-07-09, by Shinji KONO
-
power set2019-07-09, by Shinji KONO
-
recovering...2019-07-09, by Shinji KONO
-
fix some2019-07-08, by Shinji KONO
-
only ordinal-definable.agda is finished. it assmues all ZF Set are Ordinals. release2019-07-08, by Shinji KONO
-
give up2019-07-08, by Shinji KONO
-
...2019-07-08, by Shinji KONO
-
ord-Ord causes od→ord x o< od→ord y → y ∋ x,2019-07-08, by Shinji KONO
-
all done but ...2019-07-08, by Shinji KONO
-
Union again2019-07-08, by Shinji KONO
-
union remains2019-07-08, by Shinji KONO
-
Power Set2019-07-08, by Shinji KONO
-
fix or2019-07-07, by Shinji KONO
-
remove otrans again. start over2019-07-07, by Shinji KONO
-
dead end?2019-07-07, by Shinji KONO
-
...2019-07-07, by Shinji KONO
-
replace using Select2019-07-06, by Shinji KONO
-
... should use Select in Replace2019-07-06, by Shinji KONO
-
otrans in repl2019-07-06, by Shinji KONO
-
replacement in HOD2019-07-06, by Shinji KONO
-
replacement in ordinal-definable2019-07-06, by Shinji KONO
-
use OD for replace condition2019-07-06, by Shinji KONO
-
...2019-07-02, by Shinji KONO
-
new replacement axiom2019-07-02, by Shinji KONO
-
ord power set2019-07-02, by Shinji KONO
-
... dead end?2019-07-01, by Shinji KONO
-
...2019-07-01, by Shinji KONO
-
power set2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
record L2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
...2019-06-27, by Shinji KONO
-
inifinite done2019-06-26, by Shinji KONO
-
infinite2019-06-26, by Shinji KONO
-
Union done2019-06-26, by Shinji KONO
-
minimum assuption2019-06-25, by Shinji KONO
-
axiom of selection2019-06-25, by Shinji KONO
-
Select declaration2019-06-25, by Shinji KONO
-
f x d2019-06-25, by Shinji KONO
-
...2019-06-25, by Shinji KONO
-
HOD2019-06-24, by Shinji KONO
-
...2019-06-20, by Shinji KONO
-
dead end2019-06-18, by Shinji KONO
-
remove o<→c< and add otrans in OD2019-06-18, by Shinji KONO
-
dead end?2019-06-18, by Shinji KONO
-
add assumption2019-06-16, by Shinji KONO
-
add Ord Ordinal order preserving map2019-06-16, by Shinji KONO
-
power set2019-06-16, by Shinji KONO
-
...2019-06-15, by Shinji KONO
-
starting over HOD2019-06-12, by Shinji KONO
-
Added tag current for changeset a402881cc3412019-06-10, by Shinji KONO
-
add comment2019-06-10, by Shinji KONO
-
Power Set done with min-sup assumption2019-06-10, by Shinji KONO
-
...2019-06-09, by Shinji KONO
-
power set using sup on Def2019-06-09, by Shinji KONO
-
Power Set and L2019-06-08, by Shinji KONO
-
clean up2019-06-08, by Shinji KONO
-
...2019-06-08, by Shinji KONO
-
replacement2019-06-06, by Shinji KONO
-
Added tag current for changeset b4742cf4ef972019-06-05, by Shinji KONO
-
infinity axiom done2019-06-05, by Shinji KONO
-
def ord conversion2019-06-05, by Shinji KONO
-
...2019-06-05, by Shinji KONO
-
osuc work around done2019-06-05, by Shinji KONO
-
split omax?2019-06-04, by Shinji KONO
-
internal error2019-06-04, by Shinji KONO
-
omax-induction does not work2019-06-04, by Shinji KONO
-
omax ..2019-06-04, by Shinji KONO
-
...2019-06-04, by Shinji KONO
-
Union (x , y) == (x , y ) only true on infinite case2019-06-04, by Shinji KONO
-
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
-
add transfinite2019-05-16, by Shinji KONO
-
...2019-05-16, by Shinji KONO
-
...2019-05-16, by Shinji KONO
-
fix2019-05-16, by Shinji KONO
-
clean up2019-05-14, by Shinji KONO
-
...2019-05-14, by Shinji KONO
-
fix2019-05-13, by Shinji KONO
-
separete constructible set2019-05-13, by Shinji KONO
-
dead end2019-05-13, by Shinji KONO
-
dead end2019-05-13, by Shinji KONO
-
...2019-05-13, by Shinji KONO
-
add constructible set2019-05-13, by Shinji KONO
-
try to fix axiom of replacement2019-05-12, by Shinji KONO
-
fix2019-05-12, by Shinji KONO
-
...2019-05-11, by Shinji KONO
-
isEquiv and isZF2019-05-11, by Shinji KONO
-
...2019-05-11, by Shinji KONO
-
reocrd ZF2019-05-11, by Shinji KONO
-
...2019-05-08, by Shinji KONO
-
union2019-05-08, by Shinji KONO
-
Set theory in Agda2019-05-08, by Shinji KONO