From d4da381e1a780c4ec9f746facd58db3327ef4ea5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 May 2015 18:34:48 -0700 Subject: [PATCH] feat(tests/lean/run/tut_104): add extra test --- tests/lean/run/tut_104.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/lean/run/tut_104.lean b/tests/lean/run/tut_104.lean index ae626f987..754e6e9e5 100644 --- a/tests/lean/run/tut_104.lean +++ b/tests/lean/run/tut_104.lean @@ -37,6 +37,14 @@ lemma injective_eq_inj_on_univ₃ (f : A → B) : injective f = inj_on f univ := repeat (apply forall_congr; intros), rewrite *(propext !true_imp) end + +lemma injective_eq_inj_on_univ₄ (f : A → B) : injective f = inj_on f univ := + begin + esimp [injective, inj_on, univ, mem], + apply propext, + repeat (apply forall_congr; intros), + rewrite *true_imp + end end end function