From 9bea23111fd149ce4024494bf6569de736693698 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Aug 2014 17:30:59 -0700 Subject: [PATCH] feat(library/logic/connectives/basic): add not_not_em theorem Signed-off-by: Leonardo de Moura --- library/logic/connectives/basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/library/logic/connectives/basic.lean b/library/logic/connectives/basic.lean index bd3a332e9..2669b0241 100644 --- a/library/logic/connectives/basic.lean +++ b/library/logic/connectives/basic.lean @@ -141,6 +141,11 @@ or_elim H1 (assume H2 : c, or_inl H2) (assume H2 : a, or_inr (H H2)) +theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) := +assume not_em : ¬(p ∨ ¬p), + have Hnp : ¬p, from + assume Hp : p, absurd (or_inl Hp) not_em, + absurd (or_inr Hnp) not_em -- iff -- ---