inequalities for fintype.card

Stream: Is there code for X?

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

Awesome! Thanks very much for that.

[Scott Morrison]

(the sorry is no problem)

[Reid Barton]

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]

I see we used basically the same things

[Scott Morrison]

I like the calc block.

[Scott Morrison]

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.)