## Stream: maths

### Topic: size of a finite set

#### Kevin Buzzard (Jan 30 2020 at 14:21):

import data.set.finite

example (α : Type*) (S : set α) (hSf : set.finite S) (d : ℕ)
(hS : @fintype.card S (set.finite.fintype hSf) = d + 1)
(s : α) (hs : s ∈ S) :
@fintype.card (S \ {s} : set α)
(set.finite.fintype (set.finite_subset hSf \$ set.diff_subset _ _)) = d := sorry


Is this what I should be doing? I am working with subalgebras of an algebra generated by a subset and I want to use results like this, so I went with set.finite rather than finset. But I now want to prove things by induction on the size of the set and I'm running into issues such as the above.

#### Chris Hughes (Jan 30 2020 at 14:23):

There should a card function on all types, that is noncomputable and returns 0 if the set is infinite.

#### Kevin Buzzard (Jan 30 2020 at 14:24):

The type in question here is presumably subtype \alpha? I am guessing we already have some card function in the cardinal library, and then we could have some function from cardinals to nat sending anything infinite to zero?

#### Kevin Buzzard (Jan 30 2020 at 14:24):

Oh -- you mean on Type?

#### Chris Hughes (Jan 30 2020 at 14:25):

Yes. Might as well be done like that and then cardinalities of sets are defeq to the cardinality of the corresponding subtype.

Last updated: May 14 2021 at 20:13 UTC