## Stream: math-comp users

### Topic: Surjectivity

#### Pierre Jouvelot (Apr 11 2023 at 20:36):

It seems to me that the following proposition should be a case for `iinv` or other codomain-, image-, or `injective`-related library lemmas, but I'm not able to find one that seems to work:

``````Lemma f_surj
n (lt0n : 0 < n)
(T : finType) (cardT : #|T| = n.+1) (t : n.-tuple T)
(f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
g \in t -> exists i : 'I_n, f i = g.
``````

Any suggestion .... or proof that it is wrong? ;)

#### Paolo Giarrusso (Apr 11 2023 at 22:35):

Seems you can drop that T is finite, it only needs decidable equality to implement a search over I_n?

#### Paolo Giarrusso (Apr 11 2023 at 22:35):

If the search failed, that'd imply having n + 1 distinct elements of t, so you'll need a pigeonhole lemma

#### Paolo Giarrusso (Apr 11 2023 at 22:40):

I'm sorry I can't help further; but I hope that's a helpful proof sketch at least

#### Laurent Théry (Apr 12 2023 at 01:39):

The statement of surjectivity looks a bit weird to me but here is one way to prove it :

``````Lemma f_surj n (T : eqType) (t : n.-tuple T)
(f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
g \in t -> exists i : 'I_n, f i = g.
Proof.
suff <- : codom f =i t by case/codomP => i ->;  exists i.
have [|y /codomP[i ->]//||//] :=
uniq_min_size _ (_ : {subset (codom f) <= t})  _.
by rewrite map_inj_uniq // enum_uniq.
by rewrite size_map size_enum_ord size_tuple.
Qed.
``````

#### Pierre Jouvelot (Apr 12 2023 at 08:58):

Thanks a lot @Laurent Théry and @Paolo Giarrusso. The lemma is indeed a bit weird (thanks for the simplification of the hypothesis, also), since it's a somewhat generalized version of a property I need within a proof related to matching problems.

Last updated: Jul 15 2024 at 21:02 UTC