Zulip Chat Archive

Stream: new members

Topic: Question about the cardinalities of Finset and Fintype


Ching-Tsun Chou (Feb 04 2025 at 08:01):

How do I prove the following?

variable (α : Type*) [Fintype α] [DecidableEq α]

example (s : Finset α) (n : ) (h : s.card = n + 1) : n < Fin.last (Fintype.card α) := by
  sorry

My informal argument is as follows: If s has cardinality n + 1 and s is a Finset in the carrier type α, then surely the cardinality of Fintype.card α is at least n + 1and hence Fin.last (Fintype.card α) is at least n + 1 > n. Is my argument correct? What are the relevant results in mathlib I can use?

Ruben Van de Velde (Feb 04 2025 at 08:50):

Looks like your code is missing imports

Zhang Qinchuan (Feb 04 2025 at 10:17):

Ching-Tsun Chou said:

then surely the cardinality of Fintype.card α is at least n + 1

This is easy.

import Mathlib

variable (α : Type*) [Fintype α] [DecidableEq α]

example (s : Finset α) (n : ) (h : s.card = n + 1) : n + 1  Fintype.card α := by
  rw [Fintype.card,  h]
  apply Finset.card_le_card
  exact Finset.subset_univ s

Ching-Tsun Chou said:

hence Fin.last (Fintype.card α) is at least n + 1 > n.

This seems weird.

Matt Diamond (Feb 04 2025 at 17:33):

docs#Finset.card_le_univ might also help

Ching-Tsun Chou (Feb 04 2025 at 21:11):

Thanks a lot! I was able to finish the proof:

example (s : Finset α) (n : ) (h : s.card = n + 1) : n < Fin.last (Fintype.card α) := by
  have h1 := Finset.card_le_univ s
  simp [h] at h1
  have h2 : n % (Fintype.card α + 1) = n := by
    apply Nat.mod_eq_of_lt
    linarith
  apply Fin.lt_def.mpr
  simp [Fin.val_last, h2]
  linarith

It may not be the most beautiful proof, but it works.


Last updated: May 02 2025 at 03:31 UTC