Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add MndToCat and other related theorems #4242

Merged
merged 29 commits into from
Sep 28, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
efc9759
Move moel to main; add ThinCat and indiscrete category
zwang123 Sep 17, 2024
dd59b38
add thincc
zwang123 Sep 17, 2024
ed125d4
Add catcone0 to main; add catprs, prsthinc and related theorems
zwang123 Sep 18, 2024
eacc384
remove ax-un dependency in f1omo
zwang123 Sep 18, 2024
18882e4
remove ax-un for 2oexw and prsthinc
zwang123 Sep 18, 2024
68f32e5
remove ax-un and ax-pow for indthinc
zwang123 Sep 18, 2024
94f7937
shorten 2oexw
zwang123 Sep 18, 2024
a5bf4d0
add mo0sn
zwang123 Sep 19, 2024
58ccf8b
add mofasn2 and related
zwang123 Sep 19, 2024
12c113f
add mofsn3 and rename theorems xxfa* -> xxf*
zwang123 Sep 19, 2024
ae8003f
add setcthin and setc2othin
zwang123 Sep 19, 2024
889d39f
shorten proof by mof02
zwang123 Sep 19, 2024
8ac55a8
rename mofsn3 -> mofmo; and fix description
zwang123 Sep 19, 2024
4f1190f
Add ProsetToCat defining and important properties
zwang123 Sep 20, 2024
38bae43
added two redundant hypotheses to prstchom for explicitness
zwang123 Sep 20, 2024
238382a
add prstchom2ALT
zwang123 Sep 20, 2024
2ed222d
add thincn0eu and prstchom2
zwang123 Sep 20, 2024
0c1f8cd
Resolve merge conflict by incorporating both suggestions
zwang123 Sep 20, 2024
ed5216e
revive ALT theorems
zwang123 Sep 20, 2024
148e9ac
prevent basendx usage
zwang123 Sep 20, 2024
c5f8254
shorten prstchomval
zwang123 Sep 20, 2024
2ee397d
sylibda->sylbida
zwang123 Sep 20, 2024
b9220e6
Add idmon and idepi
zwang123 Sep 21, 2024
80c1fd8
add MndToCat
zwang123 Sep 21, 2024
c9e8378
add grptcmon and grptcepi
zwang123 Sep 22, 2024
3b043e4
add dtrucor3
zwang123 Sep 23, 2024
49325b7
merge develop and resolve conflict
zwang123 Sep 24, 2024
7d71ac3
fix description based on PR comments
zwang123 Sep 25, 2024
97c5446
mndtcco2: .xb -> .o. ; add monepilem to factor out common proof steps
zwang123 Sep 25, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions discouraged
289 changes: 289 additions & 0 deletions set.mm
Loading