Email Gateway (Aug 22 2022 at 14:54): Email Gateway (Aug 22 2022 at 14:54):From: Manuel Eberl <eberlm@in.tum.de>
Well, there is "inj_on g B" for saying that g is injective on B and ‘g `
B ⊆ A’ for saying that g maps every element of B to an element in A.
Obtaining that function g could be done e.g. using inv_into. ‘inv_into A
f’ is a function that fulfils ‘f (inv_into A f y) = y’ for any y in f `
A, and if f is injective on A, the equation ‘inv_into A f (f x) = x’
also holds. (cf. the lemmas f_inv_into_f and inv_into_f_f in the theory
Hilbert_Choice in Isabelle)
The definition of inv_into is straightforward: ‘inv_into A f x = SOME y.
y ∈ A ∧ f y = x’.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:54):From: "Elsa L. Gunter" <egunter@illinois.edu>
Dear Henning,
I'm not sure of the type of the thing you are requesting. There
isn't a unique function g of type B -> A such that g(f b) = b. Since
your are starting with a surjective function, you could define g using
the Hilbert Choice operator SOME by g y = SOME x. (f x = y). From
surjectivity you have for all y there exists x such the f x = y, so you
can show f (g y) = y. Otherwise, the preimage of an element of B would
be a set and you don't need surjectivity to define this since you just
get empty set for the preimage of any element not in the range.
---Elsa
Email Gateway (Aug 22 2022 at 15:00):From: "henning.seidler" <henning.seidler@mailbox.tu-berlin.de>
Hello everyone,
I have a surjection of the kind "f: A ->> B", and now I would like to obtain an injective preimage function g.
What is the best way to write this down?
Is there some short notation for "g is an injective function from B to A"?
I assume, I should write the inversion property as a separate condition.
Regards,
Henning
signature.asc
Last updated: Apr 24 2024 at 08:20 UTC