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

chore(library/data/fintype/function): fix indentation

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-27 12:32:27 -07:00
parent 766fdd415a
commit 4eafcfe945
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/data/fintype/function.lean
View file

@ -391,18 +391,18 @@ variable [finB : fintype B]
include finB
lemma surj_of_inj_eq_card : card A = card B → ∀ {f : A → B}, injective f → surjective f :=
assume Peqcard, take f, assume Pinj,
decidable.rec_on decidable_forall_finite
(assume P : surjective f, P)
(assume Pnsurj : ¬surjective f, obtain b Pne, from exists_not_of_not_forall Pnsurj,
assert Pall : ∀ a, f a ≠ b, from forall_not_of_not_exists Pne,
assert Pbnin : b ∉ image f univ, from λ Pin,
obtain a Pa, from exists_of_mem_image Pin, absurd (and.right Pa) (Pall a),
assert Puniv : finset.card (image f univ) = card A,
from card_eq_card_image_of_inj Pinj,
assert Punivb : finset.card (image f univ) = card B, from eq.trans Puniv Peqcard,
assert P : image f univ = univ, from univ_of_card_eq_univ Punivb,
absurd (P⁻¹▸ mem_univ b) Pbnin)
assume Peqcard, take f, assume Pinj,
decidable.rec_on decidable_forall_finite
(assume P : surjective f, P)
(assume Pnsurj : ¬surjective f,
obtain b Pne, from exists_not_of_not_forall Pnsurj,
assert Pall : ∀ a, f a ≠ b, from forall_not_of_not_exists Pne,
assert Pbnin : b ∉ image f univ, from λ Pin,
obtain a Pa, from exists_of_mem_image Pin, absurd (and.right Pa) (Pall a),
assert Puniv : finset.card (image f univ) = card A, from card_eq_card_image_of_inj Pinj,
assert Punivb : finset.card (image f univ) = card B, from eq.trans Puniv Peqcard,
assert P : image f univ = univ, from univ_of_card_eq_univ Punivb,
absurd (P⁻¹▸ mem_univ b) Pbnin)
end inj