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 + 1
and 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 leastn + 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 leastn + 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