Skip to content

Add section to my mathbox about 'hereditarily finite structures' - #5514

Merged
benjub merged 2 commits into
metamath:developfrom
EricSchmidt-119:hfstruct
Oct 3, 2026
Merged

benjub merged 2 commits into
metamath:developfrom
EricSchmidt-119:hfstruct

Conversation

@EricSchmidt-119

@EricSchmidt-119 EricSchmidt-119 commented Sep 30, 2026 •

Copy link
Copy Markdown
Contributor

Move fununiq from Scott Fenton's mathbox to main
Move cnvssb from Richard Penner's mathbox to main

New mathbox statements:

cocanss2
cocan2g
cocanss1
cocan1g
dmstructnn
dfstructfi
rnstructfi
chfstruct
dfhfstruct
hfstructstruct
hfstructfun
rnhfstructsshf
ishfstruct
rnhfstructhf
hfstructhf
hfstructcan

Comment thread set.mm Outdated
Comment thread set.mm
@benjub
benjub merged commit 809e7db into metamath:develop Oct 3, 2026
10 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants