size of a finite set

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

Oh -- you mean on Type?

[Chris Hughes]

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