lemma about finset cardinatlity

Stream: general

[Frederick Pu]

Is there a lemma showing that for any finite set A : Set T, there is function f : Fin A.card -> T such that Finset.image f Finset.univ = A

[Frederick Pu]

another variation is that if [LinearOrder T] then for any finite set A : Set T there is a function f : Fin A.card -> T such that StrictMono f and Finset.image f Finset.univ = A

[Eric Wieser]

Is docs#Finset.orderIsoOfFin helpful?

[Frederick Pu]

ig, but i think a lemma of the specific form im talking about could be useful

[Frederick Pu]

would it be possible to open an issue for this

[Matt Diamond]

I suppose you could do something like this:

import Mathlib

example (A : Set T) (hA : A.Finite) : ∃ (f : Fin (Nat.card A) → T), Set.range f = A :=
by
  have := hA.to_subtype
  use Subtype.val ∘ (Finite.equivFin A).symm.toFun
  simp

but then again, you could just use (Finite.equivFin A).symm directly...

[Frederick Pu]

hmm maybe there's a constructive way of making the StrictMono mapping function then

[Matt Diamond]

wouldn't Finset.orderIsoOfFin give you that mapping? I'm not sure what you're looking for

[Matt Diamond]

you could get StrictMono out of that pretty easily

[Frederick Pu]

yeah thanks! that's exactly what I'm looking for

[Frederick Pu]

is there a lemma that says orderIsoOfFin is StrictMono?

[Matt Diamond]

it's an order iso, so you can use docs#OrderIso.strictMono

[Matt Diamond]

yeah thanks! that's exactly what I'm looking for

okay cool... that was what Eric suggested above

[Yury G. Kudryashov]

See also docs#Finset.orderEmbOfFin