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

feat(library/data/finset/to_set): add to_set.inj

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-03 11:36:19 -07:00
parent 16d03c17ee
commit 2a6ea2c6fb
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/data/finset/to_set.lean
View file

@ -18,6 +18,14 @@ abbreviation ts := @to_set A
variables (s t : finset A) (x : A) variables (s t : finset A) (x : A)
theorem mem_eq_mem_to_set : (x ∈ s) = (x ∈ ts s) := rfl
definition to_set.inj {s₁ s₂ : finset A} : to_set s₁ = to_set s₂ → s₁ = s₂ :=
λ h, ext (λ a, iff.of_eq (calc
(a ∈ s₁) = (a ∈ ts s₁) : mem_eq_mem_to_set
... = (a ∈ ts s₂) : h
... = (a ∈ s₂) : mem_eq_mem_to_set))
/- operations -/ /- operations -/
theorem mem_to_set_empty : (x ∈ ts ∅) = (x ∈ ∅) := rfl theorem mem_to_set_empty : (x ∈ ts ∅) = (x ∈ ∅) := rfl
@ -50,8 +58,6 @@ theorem to_set_image {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A
/- relations -/ /- relations -/
theorem mem_eq_mem_to_set : (x ∈ s) = (x ∈ ts s) := rfl
definition decidable_mem_to_set [instance] (x : A) (s : finset A) : decidable (x ∈ ts s) := definition decidable_mem_to_set [instance] (x : A) (s : finset A) : decidable (x ∈ ts s) :=
decidable_of_decidable_of_eq _ !mem_eq_mem_to_set decidable_of_decidable_of_eq _ !mem_eq_mem_to_set