Inj_of_ncard_le

Stream: Is there code for X?

[Iván Renison]

Hi, do you know if we have code for something like this?

lemma aux2 {α β} (X : Set α) (Y : Set β) (hX : ¬IsEmpty X) (hY : ¬IsEmpty Y) :
    X.ncard ≤ Y.ncard ↔ ∃ f : α → β, Set.InjOn f X := sorry
  sorry

[Kevin Buzzard]

This won't be true as it stands because if X is infinite then X.ncard = 0. On the other hand you don't need the nonemptiness assumptions.

[Iván Renison]

And assuming finset or fintypes?

[Iván Renison]

I added ¬IsEmpty X but what I meant was Finite X :man_facepalming:

[Kevin Buzzard]

Actually you do need some kind of nonemptiness assumption because if X is empty but alpha isn't, and if beta is empty, then 0<=0 but there's no f.

[Kevin Buzzard]

@loogle Set.ncard, Set.InjOn

[loogle]

:search: Set.ncard_image_of_injOn, Set.injOn_of_ncard_image_eq, and 2 more

[Kevin Buzzard]

docs#Set.ncard_le_ncard_of_injOn is one way (and as I say the other way is false without extra assumptions) (your statement also doesn't have the claim that f sends X to Y)

[Iván Renison]

Yes, sorry, I didn't made quite the right statement, but what I want is an injection from X to Y given that the cardinal of X is less or equal than the cardinal of Y (I can assume non emptiness and finitenes)

[Iván Renison]

Maybe a f : X ↪ Y

[Kevin Buzzard]

Sure this will be in the library, in various forms. You can practice using loogle yourself to find it :-) There are lots of ways of talking about the cardinality of a set/type so there will be various different statements.

[Kevin Buzzard]

e.g. @loogle Cardinal.mk, Function.Injective

[loogle]

:search: Cardinal.mk_le_of_injective, Cardinal.lift_mk_le_lift_mk_of_injective, and 12 more

[Iván Renison]

All what I see is in one direction, taking some sort of injective function and showing something about the carnalities

[Iván Renison]

I now found Function.Embedding.exists_of_card_le_finset, which seems to be what I'm looking for. Thank you very much

[Kevin Buzzard]

This is about yet another kind of cardinality, namely docs#Fintype.card . It's kind of hopeless to answer questions of the form "what's the Lean theorem corresponding to this mathematical statement involving the size of a set" because there are so many different ways you can translate it. Usually when I'm in this situation the precise version I'm looking for is informed by the actual reason I want it (e.g. the actual goal I'm trying to solve).