# Zulip Chat Archive

## Stream: new members

### Topic: cardinality lemma for disjoint union

#### Mantas Baksys (Mar 30 2021 at 16:49):

Hi, all! I have a been on a quest to (re)prove Lagrange's Theorem in order to get to know Lean better and ran into the following lemma, which I cannot prove :

```
import data.set.finite
import init.data.set
import data.setoid.partition
import algebra.big_operators.ring
open_locale classical
open_locale big_operators
variables{α: Type*} [fintype α]
variable R: α → α → Prop
def equiv_cl (a : α) := {b : α | R b a}
variable equiv_R : equivalence R
def setoid_R: setoid α := ⟨R, equiv_R⟩
def equiv_cl_set := setoid.classes (setoid_R R equiv_R)
lemma card_Union_eq_sum_card_equiv_cl: fintype.card (⋃ a ∈ equiv_cl_set R equiv_R, a) = ∑ (x : equiv_cl_set R equiv_R), (fintype.card x) :=
begin
sorry,
end
```

Ideally, I would like apply `finset.card.bUnion`

but I cannot seem to make the types match at any rate. I'm welcome to all suggestions :smiley:

#### Alex J. Best (Mar 30 2021 at 17:04):

The trouble is coming from the fact your `equiv_cl_set`

is a set of sets, not a finset of finset, so lemmas about finsets do not apply.

#### Alex J. Best (Mar 30 2021 at 17:06):

I don't think people use `setoid.classes`

too much in mathlib, as we have quotient types explicitly working with equivalence relations as sets of sets isn't done as much I guess.

#### Alex J. Best (Mar 30 2021 at 17:06):

You could maybe set it up like this:

```
import data.set.finite
import init.data.set
import data.setoid.partition
import algebra.big_operators.ring
open_locale classical
open_locale big_operators
variables{α: Type*} [fintype α]
noncomputable theory
variables (R: α → α → Prop)
open finset
def equiv_cl (a : α) : finset α := univ.filter (R a)
def equiv_cl_set : finset (finset α) := univ.image (equiv_cl R)
```

#### Kevin Buzzard (Mar 30 2021 at 18:23):

There are so many ways to do finiteness in Lean. I'd be tempted to stick to a non-constructive one but we're only now in the process of adding all the lemmas to mathlib :-)

#### Mantas Baksys (Mar 30 2021 at 20:50):

Thanks, Alex for your response. Managed to get it all working :smiley:

#### Alex J. Best (Mar 30 2021 at 23:34):

Great, I'd recommend trying docs#quotient too to see if it makes your life easier or not. Kevin wrote a nice thing about the difference between using explicit equivalence classes and using `quotient`

at https://xenaproject.wordpress.com/2021/03/04/formalising-mathematics-workshop-7-quotients/

Last updated: Dec 20 2023 at 11:08 UTC