Zulip Chat Archive

Stream: Is there code for X?

Topic: inequalities for fintype.card


view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 22 2020 at 14:49):

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

view this post on Zulip Scott Morrison (May 22 2020 at 14:51):

Awesome! Thanks very much for that.

view this post on Zulip Scott Morrison (May 22 2020 at 14:51):

(the sorry is no problem)

view this post on Zulip 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 β : _

view this post on Zulip Reid Barton (May 22 2020 at 14:52):

I see we used basically the same things

view this post on Zulip Scott Morrison (May 22 2020 at 14:52):

I like the calc block.

view this post on Zulip 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