# Zulip Chat Archive

## 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