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

Prove that some small graphs are acyclic #3573

Merged
merged 13 commits into from
Oct 20, 2023
Merged

Conversation

BTernaryTau
Copy link
Contributor

acycgr0v

A null graph (with no vertices) is an acyclic graph.

acycgr1v

A multigraph with one vertex is an acyclic graph.

acycgr2v

A simple graph with two vertices is an acyclic graph.

prclisacycgr

A proper class (representing a null graph, see ~ vtxvalprc ) has the property of an acyclic graph (see also ~ acycgr0v ).

set.mm Show resolved Hide resolved
set.mm Show resolved Hide resolved
@wlammen
Copy link
Contributor

wlammen commented Oct 20, 2023

I don't see a good reason to keep this mathbox work longer on hold.

@wlammen wlammen merged commit 73e8833 into metamath:develop Oct 20, 2023
10 checks passed
@BTernaryTau BTernaryTau deleted the acyc branch October 21, 2023 20:17
avekens added a commit to avekens/set.mm that referenced this pull request Jan 5, 2024
Enhancement of comment for df-rn (Definition of `ran`), see also discussion in PR metamath#3741

Conventions:
* Revision of section "Distinctness or freeness": order of elements in a $d-condition (see also discussion in PR metamath#3573)

Mathboxes:
* ~mptima moved from GS's mathbox to main
* ~fproj and ~fimaproj moved from TA's mathbox to main
* ~offval0 removed from AV's mathbox (duplicate of ~offval3)

Usage of ~fpar and ~fsplit, see also discussion in PR metamath#3735
* Example ~ex-fpar for ~fpar added
* combination ~fsplitfpar of ~ fsplit and ~ fpar  added
* connection to function operation map ` oF ` added (~offsplitfpar)
@avekens avekens mentioned this pull request Jan 5, 2024
benjub pushed a commit that referenced this pull request Jan 7, 2024
* Miscellaneous

Enhancement of comment for df-rn (Definition of `ran`), see also discussion in PR #3741

Conventions:
* Revision of section "Distinctness or freeness": order of elements in a $d-condition (see also discussion in PR #3573)

Mathboxes:
* ~mptima moved from GS's mathbox to main
* ~fproj and ~fimaproj moved from TA's mathbox to main
* ~offval0 removed from AV's mathbox (duplicate of ~offval3)

Usage of ~fpar and ~fsplit, see also discussion in PR #3735
* Example ~ex-fpar for ~fpar added
* combination ~fsplitfpar of ~ fsplit and ~ fpar  added
* connection to function operation map ` oF ` added (~offsplitfpar)

* Revision after review

* comment for ~df-rn
* symbol .+ instead of O in ~offsplitfpar
* comments for ~fvproj and ~fimaproj
* explaining "implicit substitution" in convenbtions for distinct variable conditions
* reorder distinct variable conditions in ~ex-fpar
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.

6 participants