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