Zulip Chat Archive

Stream: maths

Topic: size of a finite set


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 14:24):

Oh -- you mean on Type?

view this post on Zulip 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