michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/finset/partition): improve lemmas on binary partition

Browse source
This commit is contained in:
Haitao Zhang 2015-07-16 14:13:06 -07:00
parent a04c6b0c7d
commit ca895e4901
2 changed files with 22 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/data/finset/partition.lean
View file

@ -114,13 +114,27 @@ begin rewrite [binary_union P at {1}], apply Union_union, exact binary_inter_emp
end end
open nat open nat
section
open algebra
variables {B : Type} [acmB : add_comm_monoid B]
include acmB
lemma Sum_binary_union (f : A → B) (P : A → Prop) [decP : decidable_pred P] {S : finset A} :
Sum S f = Sum {s ∈ S | P s} f + Sum {s ∈ S | ¬P s} f :=
calc
Sum S f = Sum ({s ∈ S | P s} ∪ {s ∈ S | ¬(P s)}) f : binary_union
... = Sum {s ∈ S | P s} f + Sum {s ∈ S | ¬P s} f : Sum_union f binary_inter_empty
end
lemma card_binary_Union_disjoint_sets (P : finset A → Prop) [decP : decidable_pred P] {S : finset (finset A)} : lemma card_binary_Union_disjoint_sets (P : finset A → Prop) [decP : decidable_pred P] {S : finset (finset A)} :
disjoint_sets S → Sum S card = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card := disjoint_sets S → card (Union S id) = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card :=
assume Pds, calc assume Pds, calc
Sum S card = card (Union S id) : card_Union_of_disjoint S id Pds card (Union S id)
... = card (Union {s ∈ S | P s} id ∪ Union {s ∈ S | ¬P s} id) : binary_Union = card (Union {s ∈ S | P s} id ∪ Union {s ∈ S | ¬P s} id) : binary_Union
... = card (Union {s ∈ S | P s} id) + card (Union {s ∈ S | ¬P s} id) : card_union_of_disjoint (binary_inter_empty_Union_disjoint_sets Pds) ... = card (Union {s ∈ S | P s} id) + card (Union {s ∈ S | ¬P s} id) : card_union_of_disjoint (binary_inter_empty_Union_disjoint_sets Pds)
... = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card : by rewrite [*(card_Union_of_disjoint _ id (disjoint_sets_filter_of_disjoint_sets Pds))] ... = Sum {s ∈ S | P s} card + Sum {s ∈ S | ¬P s} card : by rewrite [*(card_Union_of_disjoint _ id (disjoint_sets_filter_of_disjoint_sets Pds))]
end partition end partition
end finset end finset

5
library/theories/group_theory/action.lean
View file

@ -371,10 +371,11 @@ calc Sum _ _ = Sum (fixed_point_orbits hom H) (λ x, 1) : Sum_ext (take c Pin, o
... = card (fixed_point_orbits hom H) * 1 : Sum_const_eq_card_mul ... = card (fixed_point_orbits hom H) * 1 : Sum_const_eq_card_mul
... = card (fixed_point_orbits hom H) : mul_one (card (fixed_point_orbits hom H)) ... = card (fixed_point_orbits hom H) : mul_one (card (fixed_point_orbits hom H))
local attribute nat.comm_semiring [instance]
lemma orbit_class_equation' : card S = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card := lemma orbit_class_equation' : card S = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card :=
calc card S = Sum (orbits hom H) finset.card : orbit_class_equation calc card S = Sum (orbits hom H) finset.card : orbit_class_equation
... = Sum (fixed_point_orbits hom H) finset.card + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_binary_Union_disjoint_sets _ (equiv_class_disjoint _) ... = Sum (fixed_point_orbits hom H) finset.card + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : Sum_binary_union
... = card (fixed_point_orbits hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits ... = card (fixed_point_orbits hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : {card_fixed_point_orbits}
... = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits_eq ... = card (fixed_points hom H) + Sum {cls ∈ orbits hom H | card cls ≠ 1} card : card_fixed_point_orbits_eq
end orbit_partition end orbit_partition