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

refactor(library/data/set/finite): make proof more robust

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-31 17:26:24 -10:00
parent 92716972c0
commit 63b93cf762
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/data/set/finite.lean
View file

@ -129,23 +129,25 @@ by rewrite [-finset.to_set_upto n]; apply finite_finset
theorem to_finset_upto (n : ℕ) : to_finset {i | i < n} = finset.upto n :=
by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto)
set_option pp.notation false
theorem finite_powerset (s : set A) [fins : finite s] : finite 𝒫 s :=
assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))],
from ext (take t, iff.intro
(suppose t ∈ 𝒫 s,
assert t ⊆ s, from this,
assert finite t, from finite_subset this,
have (#finset to_finset t ∈ 𝒫 (to_finset s)),
assert (#finset to_finset t ∈ 𝒫 (to_finset s)),
by rewrite [finset.mem_powerset_iff_subset, to_finset_subset_to_finset_eq]; apply `t ⊆ s`,
assert to_finset t ∈ (finset.to_set (finset.powerset (to_finset s))), from this,
mem_image this (by rewrite to_set_to_finset))
(assume H',
obtain t' [(tmem : (#finset t' ∈ 𝒫 (to_finset s))) (teq : finset.to_set t' = t)],
from H',
show t ⊆ s,
begin
rewrite [-teq, finset.mem_powerset_iff_subset at tmem, -to_set_to_finset s],
rewrite -finset.subset_eq_to_set_subset, assumption
end)),
begin
rewrite [-teq, finset.mem_powerset_iff_subset at tmem, -to_set_to_finset s],
rewrite -finset.subset_eq_to_set_subset, assumption
end)),
by rewrite H; apply finite_image
/- induction for finite sets -/