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

feat(library/standard/logic): mark 'not equal' as an abbreviation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-24 12:01:09 -07:00
parent 2eb84c5f74
commit 08174f904b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/standard/logic.lean
View file

@ -160,7 +160,7 @@ theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c
:= assume Ha, H2 (H1 ◂ Ha)
definition ne {A : Type} (a b : A) := ¬(a = b)
definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
infix `≠`:50 := ne
theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b