cardinality lemma for disjoint union

Stream: new members

[Mantas Baksys]

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]

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]

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]

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]

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]

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

[Alex J. Best]

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/