## Stream: Is there code for X?

### Topic: inequalities for fintype.card

#### Scott Morrison (May 22 2020 at 14:37):

I need something along the lines of

lemma card_lt_card_of_injective_of_not_mem
{α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
(b : β) (w : b ∉ set.range f) : fintype.card α < fintype.card β :=


Any advice on how to get this from library material?

#### Scott Morrison (May 22 2020 at 14:40):

My plan would be to prove fintype.card α ≤ fintype.card β from function.injective f, then case split and in the case fintype.card α = fintype.card β show that f is an equivaelence, and obtain a contradiction from w. That all seems doable, but .... I wish it were easier!

#### Bhavik Mehta (May 22 2020 at 14:49):

import data.fintype.basic

open finset

lemma card_lt_card_of_injective_of_not_mem
{α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
(b : β) (w : b ∉ set.range f) : fintype.card α < fintype.card β :=
begin
classical,
rw [← card_univ, ← card_image_of_injective univ h, ← card_univ],
apply card_lt_card,
rw ssubset_iff,
refine ⟨b, _, subset_univ _⟩,
sorry,
end


#### Bhavik Mehta (May 22 2020 at 14:49):

Here's an approach with one sorry which might be a bit easier

#### Scott Morrison (May 22 2020 at 14:51):

Awesome! Thanks very much for that.

#### Scott Morrison (May 22 2020 at 14:51):

(the sorry is no problem)

#### Reid Barton (May 22 2020 at 14:51):

Maybe something like

import data.fintype.card

open finset
open_locale classical

lemma card_lt_card_of_injective_of_not_mem
{α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
(b : β) (w : b ∉ set.range f) : fintype.card α < fintype.card β :=
calc
fintype.card α = (univ : finset α).card : _
... = (image f univ).card : (card_image_of_injective univ h).symm
... < (insert b (image f univ)).card : card_lt_card (ssubset_insert _)
... ≤ (univ : finset β).card : _
... = fintype.card β : _


#### Reid Barton (May 22 2020 at 14:52):

I see we used basically the same things

#### Scott Morrison (May 22 2020 at 14:52):

I like the calc block.

#### Scott Morrison (May 22 2020 at 14:57):

import data.fintype.card

open finset
open_locale classical

lemma card_lt_card_of_injective_of_not_mem
{α β : Type*} [fintype α] [fintype β] (f : α → β) (h : function.injective f)
(b : β) (w : b ∉ image f univ) : fintype.card α < fintype.card β :=
calc
fintype.card α = (univ : finset α).card : rfl
... = (image f univ).card : (card_image_of_injective univ h).symm
... < (insert b (image f univ)).card : card_lt_card (ssubset_insert w)
... ≤ (univ : finset β).card : card_le_of_subset (subset_univ _)
... = fintype.card β : rfl


completes the gaps in Reid's version. (And cheats by changing the type of w.)

Last updated: May 16 2021 at 05:21 UTC