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

feat(library/data/finset/card): add eq_of_card_eq_of_subset theorem

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-19 19:35:13 -07:00
parent 2910c780d0
commit ee0d919c6f
2 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/data/finset/basic.lean
View file

@ -553,6 +553,15 @@ subset_of_forall (take x, assume H : x ∈ s, mem_insert_of_mem _ H)
theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ := theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H)) ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H))
section
variable [decA : decidable_eq A]
include decA
theorem erase_subset_erase_of_subset {a : A} {s₁ s₂ : finset A} : s₁ ⊆ s₂ → erase a s₁ ⊆ erase a s₂ :=
λ is_sub, subset_of_forall (λ b bin,
mem_erase_of_ne_of_mem (ne_of_mem_erase bin) (mem_of_subset_of_mem is_sub (mem_of_mem_erase bin)))
end
/- upto -/ /- upto -/
section upto section upto
definition upto (n : nat) : finset nat := definition upto (n : nat) : finset nat :=

20
library/data/finset/card.lean
View file

@ -190,4 +190,24 @@ finset.induction_on s
card_union_of_disjoint H8, H6]) card_union_of_disjoint H8, H6])
end deceqB end deceqB
lemma eq_of_card_eq_of_subset {s₁ s₂ : finset A} : card s₁ = card s₂ → s₁ ⊆ s₂ → s₁ = s₂ :=
have aux : ∀ (n : nat) (s₁ s₂ : finset A), card s₁ = n → card s₂ = n → s₁ ⊆ s₂ → s₁ = s₂,
begin
clear s₁ s₂,
intro n, induction n with n ih,
{intro s₁ s₂ e₁ e₂ is_sub, rewrite [empty_of_card_eq_zero e₁, empty_of_card_eq_zero e₂] },
{intro s₁ s₂ e₁ e₂ is_sub,
have ne : s₁ ≠ ∅, from non_empty_of_card_succ e₁,
cases (exists_of_not_empty ne) with a ains₁,
have ains₂ : a ∈ s₂, from mem_of_subset_of_mem is_sub ains₁,
have e₁' : card (erase a s₁) = n, by rewrite [card_erase_of_mem ains₁, e₁],
have e₂' : card (erase a s₂) = n, by rewrite [card_erase_of_mem ains₂, e₂],
have is_sub' : erase a s₁ ⊆ erase a s₂, from erase_subset_erase_of_subset is_sub,
have eq₁ : erase a s₁ = erase a s₂, from ih _ _ e₁' e₂' is_sub',
have eq₂ : insert a (erase a s₁) = insert a (erase a s₂), by rewrite eq₁,
rewrite [insert_erase ains₁ at eq₂, insert_erase ains₂ at eq₂],
exact eq₂}
end,
λ e h, aux (card s₂) s₁ s₂ e rfl h
end finset end finset