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

fix(library/data/countable): typos

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-14 21:26:56 -07:00
parent 9534cfe92f
commit 039f1de524
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/countable.lean
View file

@ -68,7 +68,7 @@ theorem unpickle_pickle_sum : ∀ s : sum A B, unpickle_sum (pickle_sum s) = som
mul_div_cancel_left _ aux₁, countable.picklek] mul_div_cancel_left _ aux₁, countable.picklek]
end end
definition countable_sum [instance] {A B : Type} [h₁ : countable A] [h₂ : countable B] : countable (sum A B) := definition countable_sum [instance] : countable (sum A B) :=
countable.mk countable.mk
(λ s, pickle_sum s) (λ s, pickle_sum s)
(λ n, unpickle_sum n) (λ n, unpickle_sum n)
@ -105,7 +105,7 @@ theorem unpickle_pickle_prod : ∀ p : A × B, unpickle_prod (pickle_prod p) = s
rewrite [*countable.picklek] rewrite [*countable.picklek]
end end
definition countable_product [instance] {A B : Type} [h₁ : countable A] [h₂ : countable B] : countable (A × B) := definition countable_product [instance] : countable (A × B) :=
countable.mk countable.mk
pickle_prod pickle_prod
unpickle_prod unpickle_prod
@ -181,7 +181,7 @@ begin
apply unpickle_pickle_list_core apply unpickle_pickle_list_core
end end
definition countable_list [instance] {A : Type} [h : countable A] : countable (list A) := definition countable_list [instance] : countable (list A) :=
countable.mk countable.mk
pickle_list pickle_list
unpickle_list unpickle_list