Miscellaneous

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 · Jan 5, 2024 · bf1fda4 · bf1fda4
1 parent 8de506c
commit bf1fda4
Show file tree

Hide file tree

Showing 2 changed files with 178 additions and 93 deletions.
diff --git a/changes-set.txt b/changes-set.txt
@@ -83,6 +83,9 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 4-Jan-24 fimaproj  [same]      moved from TA's mathbox to main set.mm
+ 4-Jan-24 fproj     [same]      moved from TA's mathbox to main set.mm
+ 4-Jan-24 mptima    [same]      moved from GS's mathbox to main set.mm
 29-Dec-23 uzidd     [same]      moved from GS's mathbox to main set.mm
 28-Dec-23 eqri      [same]      moved from TA's mathbox to main set.mm
 28-Dec-23 domep     dmep        moved from SF's mathbox to main set.mm