preimages, decompositions of function into a surjective and an injective function #3877
Conversation
…ive function Main: * ~iuneqconst added * ~uniexd moved from GS' mathbox AV's mathbox: * auxiliary theorems for (pre)images * theorems for the set of all preimages of function values * decomposition of function into a surjective and an injective function with images as domain of the injective function
| -> ( A. x e. S ( F ` x ) = ( F ` X ) | ||
| -> U. ( F " S ) = ( F ` X ) ) ) $= | ||
| ( vy wf wss wcel w3a cv cfv wceq wral cima cuni wa ciun wfun 3ad2ant1 syl | ||
| ffun adantr funiunfv simp3 fveqeq2 cbvralv biimpi fveq2 iuneqconst syl2an |
There was a problem hiding this comment.
you can use cbvralvw instead of cbvralv here, which will let you avoid ax-13 without adding any extra dv conditions:
${
$d F x y $. $d S x y $. $d X x y $.
$( The union of the image of a subset ` S ` of the domain of a Function
with elements having the same function value is the function value at
one of the elements of ` S ` . (Contributed by AV, 5-Mar-2024.) $)
uniimafveqt $p |- ( ( F : A --> B /\ S C_ A /\ X e. S )
-> ( A. x e. S ( F ` x ) = ( F ` X )
-> U. ( F " S ) = ( F ` X ) ) ) $=
( vy wf wss wcel w3a cv cfv wceq wral cima cuni wa ciun wfun 3ad2ant1 syl
ffun adantr funiunfv simp3 cbvralvw biimpi fveq2 iuneqconst syl2an eqtr3d
fveqeq2 ex ) BCEHZDBIZFDJZKZALZEMFEMZNZADOZEDPQZUTNURVBRZGDGLZEMZSZVCUTVD
ETZVGVCNURVHVBUOUPVHUQBCEUCUAUDGDEUEUBURUQVFUTNZGDOZVGUTNVBUOUPUQUFVBVJVA
VIAGDUSVEUTEUMUGUHGDVFUTFVEFEUIUJUKULUN $.
$}
Actually, I think cbvralv should be discouraged, and we should invite people to use cbvralvw instead.
There was a problem hiding this comment.
I like the idea of making this a discouragement tag if we expect people to follow this practice generally.
There was a problem hiding this comment.
Done - I do not know if this was discussed already before (maybe in Google group: https://groups.google.com/g/metamath/c/OB2_9sYgDfA.?), but I would also endorse to tag cbvralv and cbvrexv (are there more?) as "discouraged".
There was a problem hiding this comment.
The discouraged tag is very prohibitive. The kind of problem given here appears very often: alrimi vs alrimih, nfsb vs nfsbv and so on, from a very long (and long standing) list. The idea behind any of them is that more distinct variables allow for a smaller axiom footprint. Or: more axioms can provide a more general theorem, which is also a valuable goal.
Here we have the situation that the dv conditions already stated allow for the narrower theorem. What you need is a kind of pick list in your proof designer, that displays close variants of a theorem, and where you easily find the best choice. Without such an assistant all you can do is improve on documentation. It would be helpful if you see an overview of variants in a particular location, maybe a doc only web page like "mathbox", but dedicated to cbvral* versions, and named like cbvral-doc, and each variant links to it
There was a problem hiding this comment.
@GinoGiotto has spent a lot of effort to remove references to ax-13.
If the cbvralv variant is not discouraged, then it's like trying to fill a leaky bucket: references to ax-13 will always come back. So I'd also be in favor of marking cbvralv as discouraged in profit of cbvralvw, instead of checking every new incoming PR.
Said differently, if both theorems are applicable, which would be a reason to use cbvralv over cbvralvw?
There was a problem hiding this comment.
if both theorems are applicable, which would be a reason to use cbvralv over cbvralvw?
There is no reason to use cbvralv without any advantage. I looked at a random subset of its applications and found no instance, where it was not replaceable. So maybe, cbvralv has no other value than stating that one dv condition in theory is unnecessary (but in practice no one cares).
But this is not an isolated problem. In this PR alone we have another candidate cbvrexv, where we can start the discussion over again. And far more need such considerations, not only with respect to ax-13, but other axioms as well. So simply discouraging anything but the variant with most dv restrictions is not a viable option, in my eyes.
As always, you need to look out for optimizations yourself, and within a mathbox you are free to just sketch a proof. Only when you move sth to main, some care is in order.
I myself put a theorem wl-cbvalsbi into my mathbox, with unnecessary ax-10 and ax-12 references in its proof, only to improve on it later.
That's the way work is done up to now.
Given that an unnecessary reference to ax-13 is a magnitude more likely than to, say, ax-11, what do you think of extending the $j annotation to mark a deliberate use of ax-13? $j need ax-13 $. for example. And a verifier that checks the simultaneous presence of ax-13 in the axiom list and this annotation.
There was a problem hiding this comment.
Done - I do not know if this was discussed already before (maybe in Google group: groups.google.com/g/metamath/c/OB2_9sYgDfA.?)
This hasn't been discussed yet, but looking at the discussion above it seems this topic deserves its own issue.
Given that ax-13 usage has recently reached an all time low, I would like to have some verification system that it will stay low, not only in the near future, but possibily in the years to come. If we don't do anything about it, I can assure you ax-13 usage will rise again. I've been collecting data about ax-13 usage for a while now. The lesson I've derived is: if you don't systematically check for something, undesired trends will show up, even if small or temporary (and they are usually temporary only because there is someone that checks for it afterwards, which should not be taken for granted).
I'm not particularly attached to the discouragement system to check for this metric, it's just the easiest tool it is currently available for us. If someone decides to show up and build a tool just for this problem, I'm not against it, on the contrary. But it has to be automatic and systematic, human review is not enough.
I don't want to give the impression that using ax-13 is prohibited. In the end, axioms are there to be used. I want to avoid the scenario in which ax-13 is used without awareness. So rather than a prohibition issue this is a communication issue. We need to find a way to communicate the user "hey, it seems you're trying to build your proof using ax-13. Did you know that about 97% of theorems in the database don't need it? Perhaps yours doesn't need it too."
Wolf Lammen is right to say that this problem does not only affects cbvralv or cbvrexv, this affects dozens of theorems, so either we are down to add about a hundred or so of discouragement tags (personally I don't have a problem with that), or we build something else. The worst decision in my opinion is to leave the state of the art as it is.
There was a problem hiding this comment.
Another way to mark theorems using ax-13 is a suffix "-a13" on their names, cbvralv becomes cbvralv-a13. This encourages to check whether another variant is more appropriate in a given proof step. Any theorem relying on a theorem with such a suffix is required to inherit this suffix.
A stand-alone verifier is easier to write in this case. It isolates the theorem name and checks it with the theorem list of the proof
There was a problem hiding this comment.
if you don't systematically check for something, undesired trends will show up, even if small or temporary
It will take some time, sure, but maybe after a while people will routinely carry out checks of this kind? There is evidence for this in the history of Metamath, which has seen some evolvement with deprecating patterns.
* uniimafveqt, imaelsetpreimafv, fundcmpsurinj * fiunlem
|
In addition to the new theorems, I replaced cbvrexv by cbvrexvw also in fiunlem. |
Just above fiunlem there are already fiunlemw , fiunw , f1iunw which are the correspoinding versions without ax-13. I'd suggest to replace your proofs with mine in the default versions, copy the dv conditions and delete my versions. Keep the original comments and credits (yours and mario), my edit is so small anyway that doesn't require to change them. |
* proofs of fiunw/f1iunw copied to fiun/f1iun * fiunlemw/fiunw/f1iunw deleted * fiunw/f1iunw replaced by fiun/f1iun in proofs of ackbij2 and All mentioned theorems do not depend on ax-13.
Done. I think we should stop additional cleanups about ax-13 in this PR now, and should continue the discussion how to avoid new usages of ax-13 in the future somewhere else. Maybe an issue can/should be opend for this: @GinoGiotto would you open it, please, and move the corresponding discussions from here to there? |
I opened an issue in #3879. |
…unctions. * funfvima2d (slightly revised and) moved from SP's mathbox to main set.mm (~imo72b2lem1 could have been shortened) * ~uniimaelsetpreimafv revised (generalized) * new theorem ~imasetpreimafvbij and corresponding new lemmas ~imasetpreimafvbijlemf, ~imasetpreimafvbijlemfo * lemma ~fundcmpsurinjlem6 revised and renamed to ~imasetpreimafvbijlemf1 * new theorems ~fundcmpsurbijinjpreimafv and ~fundcmpsurbijinj * proof of ~fundcmpsurinjpreimafv shortened using ~fundcmpsurbijinjpreimafv
|
As Gérard Lang observed, the mapping of the set of all preimages of values of a function onto the range of the function is bijective (see ~ imasetpreimafvbij ). By this, it can be shown that every function From this, both variants of decompositions of a function into a surjective and an injective function can be derived: Let These additional theorems (and the modification of existing theorems necessary or helpful to prove these) are contained in the latest (and hopefully final) commit of this PR. |
|
@tirix and @GinoGiotto could you have a look at the latest commit 9851ad8, please? |
| $d S x z $. $d X x $. $d Y x $. | ||
| $( An element of the preimage of a function value is an element of the | ||
| domain of the function with the same value as another element of the | ||
| premimage. (Contributed by AV, 9-Mar-2024.) $) |
Inspired by Gérard Lang, I proved that an arbitrary function can be decomposed into a surjective and an injective function in two different ways. The variant using the images as domain of the injective function was very easy, the other variant using the preimages as domain of the injective function was not so easy, at least to prove it formally. A lot of auxiliary theorems were necessary to achieve this.
For more information see section header comment of section "Preimages of function values" in my mathbox.
Details:
Main:
AV's mathbox: